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