Metamath Proof Explorer

Theorem zfcndrep

Description: Axiom of Replacement ax-rep , reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Aug-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion zfcndrep ⊢ ∀ w ∃ y ∀ z ∀ y φ → z = y → ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ

Proof

Step Hyp Ref Expression
1 nfe1 ⊢ Ⅎ y ∃ y ∀ z ∀ y φ → z = y
2 nfv ⊢ Ⅎ y z ∈ w
3 nfv ⊢ Ⅎ y w ∈ x
4 nfa1 ⊢ Ⅎ y ∀ y ∀ y φ
5 3 4 nfan ⊢ Ⅎ y w ∈ x ∧ ∀ y ∀ y φ
6 5 nfex ⊢ Ⅎ y ∃ w w ∈ x ∧ ∀ y ∀ y φ
7 2 6 nfbi ⊢ Ⅎ y z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
8 7 nfal ⊢ Ⅎ y ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
9 1 8 nfim ⊢ Ⅎ y ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
10 9 nfex ⊢ Ⅎ y ∃ w ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
11 elequ2 ⊢ y = x → w ∈ y ↔ w ∈ x
12 11 anbi1d ⊢ y = x → w ∈ y ∧ ∀ y ∀ y φ ↔ w ∈ x ∧ ∀ y ∀ y φ
13 12 exbidv ⊢ y = x → ∃ w w ∈ y ∧ ∀ y ∀ y φ ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
14 13 bibi2d ⊢ y = x → z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ ↔ z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
15 14 albidv ⊢ y = x → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ ↔ ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
16 15 imbi2d ⊢ y = x → ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ ↔ ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
17 16 exbidv ⊢ y = x → ∃ w ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ ↔ ∃ w ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
18 axrepnd ⊢ ∃ w ∃ y ∀ z ∀ y φ → z = y → ∀ z ∀ y z ∈ w ↔ ∃ w ∀ z w ∈ y ∧ ∀ y ∀ y φ
19 19.3v ⊢ ∀ y z ∈ w ↔ z ∈ w
20 19.3v ⊢ ∀ z w ∈ y ↔ w ∈ y
21 20 anbi1i ⊢ ∀ z w ∈ y ∧ ∀ y ∀ y φ ↔ w ∈ y ∧ ∀ y ∀ y φ
22 21 exbii ⊢ ∃ w ∀ z w ∈ y ∧ ∀ y ∀ y φ ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ
23 19 22 bibi12i ⊢ ∀ y z ∈ w ↔ ∃ w ∀ z w ∈ y ∧ ∀ y ∀ y φ ↔ z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ
24 23 albii ⊢ ∀ z ∀ y z ∈ w ↔ ∃ w ∀ z w ∈ y ∧ ∀ y ∀ y φ ↔ ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ
25 24 imbi2i ⊢ ∃ y ∀ z ∀ y φ → z = y → ∀ z ∀ y z ∈ w ↔ ∃ w ∀ z w ∈ y ∧ ∀ y ∀ y φ ↔ ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ
26 25 exbii ⊢ ∃ w ∃ y ∀ z ∀ y φ → z = y → ∀ z ∀ y z ∈ w ↔ ∃ w ∀ z w ∈ y ∧ ∀ y ∀ y φ ↔ ∃ w ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ
27 18 26 mpbi ⊢ ∃ w ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ y ∧ ∀ y ∀ y φ
28 10 17 27 chvar ⊢ ∃ w ∃ y ∀ z ∀ y φ → z = y → ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
29 28 19.35i ⊢ ∀ w ∃ y ∀ z ∀ y φ → z = y → ∃ w ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ
30 nfv ⊢ Ⅎ w z ∈ y
31 nfe1 ⊢ Ⅎ w ∃ w w ∈ x ∧ ∀ y φ
32 30 31 nfbi ⊢ Ⅎ w z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
33 32 nfal ⊢ Ⅎ w ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
34 elequ2 ⊢ w = y → z ∈ w ↔ z ∈ y
35 nfa1 ⊢ Ⅎ y ∀ y φ
36 35 19.3 ⊢ ∀ y ∀ y φ ↔ ∀ y φ
37 36 anbi2i ⊢ w ∈ x ∧ ∀ y ∀ y φ ↔ w ∈ x ∧ ∀ y φ
38 37 exbii ⊢ ∃ w w ∈ x ∧ ∀ y ∀ y φ ↔ ∃ w w ∈ x ∧ ∀ y φ
39 38 a1i ⊢ w = y → ∃ w w ∈ x ∧ ∀ y ∀ y φ ↔ ∃ w w ∈ x ∧ ∀ y φ
40 34 39 bibi12d ⊢ w = y → z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ ↔ z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
41 40 albidv ⊢ w = y → ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ ↔ ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
42 8 33 41 cbvexv1 ⊢ ∃ w ∀ z z ∈ w ↔ ∃ w w ∈ x ∧ ∀ y ∀ y φ ↔ ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
43 29 42 sylib ⊢ ∀ w ∃ y ∀ z ∀ y φ → z = y → ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ