Theorem axrep1

Description: The version of the Axiom of Replacement used in the Metamath Solitaire applet https://us.metamath.org/mmsolitaire/mms.html . Equivalence is shown via the path ax-rep -> axrep1 -> axrep2 -> axrepnd -> zfcndrep = ax-rep . (Contributed by NM, 19-Nov-2005) (Proof shortened by Mario Carneiro, 17-Nov-2016) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

	Ref	Expression
Assertion	axrep1	⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elequ2	⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
2	1	anbi1d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
3	2	exbidv	⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
4	3	bibi2d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) )
5	4	albidv	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) )
6	5	exbidv	⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) )
7	6	imbi2d	⊢ ( 𝑤 = 𝑦 → ( ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) ↔ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) ) )
8		ax-rep	⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) )
9		19.3v	⊢ ( ∀ 𝑦 𝜑 ↔ 𝜑 )
10	9	imbi1i	⊢ ( ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ( 𝜑 → 𝑧 = 𝑦 ) )
11	10	albii	⊢ ( ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) )
12	11	exbii	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) )
13	12	albii	⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) )
14		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ 𝑦
15		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 )
16	14 15	nfbi	⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) )
17	16	nfal	⊢ Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) )
18		nfv	⊢ Ⅎ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
19		elequ2	⊢ ( 𝑦 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑥 ) )
20	9	anbi2i	⊢ ( ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
21	20	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
22	21	a1i	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
23	19 22	bibi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) )
24	23	albidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) )
25	17 18 24	cbvexv1	⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
26	8 13 25	3imtr3i	⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
27	7 26	chvarvv	⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
28	27	19.35ri	⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )