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

Metamath Proof Explorer

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