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