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