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 x y z φ z = y z z x x x y φ

Proof

Step Hyp Ref Expression
1 elequ2 w = y x w x y
2 1 anbi1d w = y x w φ x y φ
3 2 exbidv w = y x x w φ x x y φ
4 3 bibi2d w = y z x x x w φ z x x x y φ
5 4 albidv w = y z z x x x w φ z z x x x y φ
6 5 exbidv w = y x z z x x x w φ x z z x x x y φ
7 6 imbi2d w = y x y z φ z = y x z z x x x w φ x y z φ z = y x z z x x x y φ
8 ax-rep x y z y φ z = y y z z y x x w y φ
9 19.3v y φ φ
10 9 imbi1i y φ z = y φ z = y
11 10 albii z y φ z = y z φ z = y
12 11 exbii y z y φ z = y y z φ z = y
13 12 albii x y z y φ z = y x y z φ z = y
14 nfv x z y
15 nfe1 x x x w y φ
16 14 15 nfbi x z y x x w y φ
17 16 nfal x z z y x x w y φ
18 nfv y z z x x x w φ
19 elequ2 y = x z y z x
20 9 anbi2i x w y φ x w φ
21 20 exbii x x w y φ x x w φ
22 21 a1i y = x x x w y φ x x w φ
23 19 22 bibi12d y = x z y x x w y φ z x x x w φ
24 23 albidv y = x z z y x x w y φ z z x x x w φ
25 17 18 24 cbvexv1 y z z y x x w y φ x z z x x x w φ
26 8 13 25 3imtr3i x y z φ z = y x z z x x x w φ
27 7 26 chvarvv x y z φ z = y x z z x x x y φ
28 27 19.35ri x y z φ z = y z z x x x y φ