Theorem example-E5.04a 675

Description: Convert Axiom of Replacement to Prenex Form.

The hypothesis imples we can construct an alternate function, '𝜑₂'. We first replace '𝑥' with '𝑥₁' in '𝜑' to obtain '𝜑₁', then we replace '𝑦' with '𝑦₁' in '𝜑₁' to obtain '𝜑₂'.

Since '𝑥₁' and '𝑦₁' are fresh variables replacing '𝑥' and '𝑦', we need the disjoint variable conditions...

$d 𝜑 𝑥₁ 𝑦₁ $. $d 𝜑₁ 𝑥 𝑦₁ $. $d 𝜑₂ 𝑥 𝑦 $.

The other condition, that neither '𝑧' nor '𝑎' should appear in '𝜑' (and by extension '𝜑₁' and '𝜑₂'), is simply part of the hypothesis for with this version of the Axiom of Replacement.

Hypotheses

Ref	Expression
example-E5.04a.1	⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))
example-E5.04a.2	⊢ (𝑦 = 𝑦₁ → (𝜑₁ ↔ 𝜑₂))
example-E5.04a.3	⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑎∀𝑥∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))

Assertion

Ref	Expression
example-E5.04a	⊢ ∃𝑎∀𝑥∀𝑦∃𝑥₁∀𝑧∃𝑦₁((𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))

Distinct variable groups:   𝜑,𝑥₁   𝜑₁,𝑥   𝜑₂,𝑥   𝜑,𝑦₁   𝜑₁,𝑦₁   𝜑₂,𝑦   𝜑,𝑧,𝑎   𝜑₁,𝑧,𝑎   𝜑₂,𝑧,𝑎   𝑥,𝑥₁,𝑦,𝑦₁,𝑧,𝑎,𝑏

Proof of Theorem example-E5.04a

Step	Hyp	Ref	Expression
1		example-E5.04a.3	. . . . . . . 8 ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑎∀𝑥∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))
2		example-E5.04a.1	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))
3	2	subiml-P3.40a 325	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑥₁ → ((𝜑 → 𝑦 = 𝑧) ↔ (𝜑₁ → 𝑦 = 𝑧)))
4	3	suballv-P5 623	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑥₁ → (∀𝑦(𝜑 → 𝑦 = 𝑧) ↔ ∀𝑦(𝜑₁ → 𝑦 = 𝑧)))
5	4	subexv-P5 624	. . . . . . . . . 10 ⊢ (𝑥 = 𝑥₁ → (∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) ↔ ∃𝑧∀𝑦(𝜑₁ → 𝑦 = 𝑧)))
6	5	cbvallv-P5 659	. . . . . . . . 9 ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) ↔ ∀𝑥₁∃𝑧∀𝑦(𝜑₁ → 𝑦 = 𝑧))
7		example-E5.04a.2	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑦₁ → (𝜑₁ ↔ 𝜑₂))
8		rcp-NDASM1of1 192	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑦₁ → 𝑦 = 𝑦₁)
9	8	subeql-P5 632	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑦₁ → (𝑦 = 𝑧 ↔ 𝑦₁ = 𝑧))
10	7, 9	subimd-P3.40c 329	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑦₁ → ((𝜑₁ → 𝑦 = 𝑧) ↔ (𝜑₂ → 𝑦₁ = 𝑧)))
11	10	cbvallv-P5 659	. . . . . . . . . . 11 ⊢ (∀𝑦(𝜑₁ → 𝑦 = 𝑧) ↔ ∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧))
12	11	subexinf-P5 608	. . . . . . . . . 10 ⊢ (∃𝑧∀𝑦(𝜑₁ → 𝑦 = 𝑧) ↔ ∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧))
13	12	suballinf-P5 594	. . . . . . . . 9 ⊢ (∀𝑥₁∃𝑧∀𝑦(𝜑₁ → 𝑦 = 𝑧) ↔ ∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧))
14	6, 13	bitrns-P3.33c.RC 303	. . . . . . . 8 ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) ↔ ∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧))
15	1, 14	subiml2-P4.RC 541	. . . . . . 7 ⊢ (∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∃𝑎∀𝑥∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))
16		qceximrv-P5 672	. . . . . . 7 ⊢ ((∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∃𝑎∀𝑥∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑎(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑥∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
17	15, 16	bimpf-P4.RC 532	. . . . . 6 ⊢ ∃𝑎(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑥∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))
18		qcallimrv-P5 671	. . . . . . 7 ⊢ ((∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑥∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑥(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
19	18	subexinf-P5 608	. . . . . 6 ⊢ (∃𝑎(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑥∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑎∀𝑥(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
20	17, 19	bimpf-P4.RC 532	. . . . 5 ⊢ ∃𝑎∀𝑥(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))
21		qcallimrv-P5 671	. . . . . . 7 ⊢ ((∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑦(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
22	21	suballinf-P5 594	. . . . . 6 ⊢ (∀𝑥(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑥∀𝑦(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
23	22	subexinf-P5 608	. . . . 5 ⊢ (∃𝑎∀𝑥(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → ∀𝑦(𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑎∀𝑥∀𝑦(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
24	20, 23	bimpf-P4.RC 532	. . . 4 ⊢ ∃𝑎∀𝑥∀𝑦(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))
25		qcallimlv-P5 673	. . . . . . 7 ⊢ ((∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑥₁(∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
26	25	suballinf-P5 594	. . . . . 6 ⊢ (∀𝑦(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑦∃𝑥₁(∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
27	26	suballinf-P5 594	. . . . 5 ⊢ (∀𝑥∀𝑦(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑥∀𝑦∃𝑥₁(∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
28	27	subexinf-P5 608	. . . 4 ⊢ (∃𝑎∀𝑥∀𝑦(∀𝑥₁∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑎∀𝑥∀𝑦∃𝑥₁(∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
29	24, 28	bimpf-P4.RC 532	. . 3 ⊢ ∃𝑎∀𝑥∀𝑦∃𝑥₁(∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))
30		qceximlv-P5 674	. . . . . . 7 ⊢ ((∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
31	30	subexinf-P5 608	. . . . . 6 ⊢ (∃𝑥₁(∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑥₁∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
32	31	suballinf-P5 594	. . . . 5 ⊢ (∀𝑦∃𝑥₁(∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑦∃𝑥₁∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
33	32	suballinf-P5 594	. . . 4 ⊢ (∀𝑥∀𝑦∃𝑥₁(∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑥∀𝑦∃𝑥₁∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
34	33	subexinf-P5 608	. . 3 ⊢ (∃𝑎∀𝑥∀𝑦∃𝑥₁(∃𝑧∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑎∀𝑥∀𝑦∃𝑥₁∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
35	29, 34	bimpf-P4.RC 532	. 2 ⊢ ∃𝑎∀𝑥∀𝑦∃𝑥₁∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))
36		qcallimlv-P5 673	. . . . . . 7 ⊢ ((∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑦₁((𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
37	36	suballinf-P5 594	. . . . . 6 ⊢ (∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑧∃𝑦₁((𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
38	37	subexinf-P5 608	. . . . 5 ⊢ (∃𝑥₁∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑥₁∀𝑧∃𝑦₁((𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
39	38	suballinf-P5 594	. . . 4 ⊢ (∀𝑦∃𝑥₁∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑦∃𝑥₁∀𝑧∃𝑦₁((𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
40	39	suballinf-P5 594	. . 3 ⊢ (∀𝑥∀𝑦∃𝑥₁∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∀𝑥∀𝑦∃𝑥₁∀𝑧∃𝑦₁((𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
41	40	subexinf-P5 608	. 2 ⊢ (∃𝑎∀𝑥∀𝑦∃𝑥₁∀𝑧(∀𝑦₁(𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))) ↔ ∃𝑎∀𝑥∀𝑦∃𝑥₁∀𝑧∃𝑦₁((𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎))))
42	35, 41	bimpf-P4.RC 532	1 ⊢ ∃𝑎∀𝑥∀𝑦∃𝑥₁∀𝑧∃𝑦₁((𝜑₂ → 𝑦₁ = 𝑧) → (𝑥 ∈ 𝑏 → (𝜑 → 𝑦 ∈ 𝑎)))

Syntax hints:  term-obj 1   = wff-equals 6   ∈ wff-elemof 7  ∀wff-forall 8   → wff-imp 10   ↔ wff-bi 104  ∃wff-exists 595

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596

This theorem is referenced by: (None)