This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )

Proof

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