Theorem axrep1 2749

Description: The version of the Axiom of Replacement used in the Metamath Solitaire applet http://us.metamath.org/mmsolitaire/mms.html. Equivalence is shown via the path ax-rep 2748 -> axrep1 2749 -> axrep2 2750 -> axrepnd 5011 -> zfcndrep 5031 = ax-rep 2748.

Assertion

Ref	Expression
axrep1	|- E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ ph)))

Distinct variable groups:   ph,y   x,y,z

Proof of Theorem axrep1

Step	Hyp	Ref	Expression
1		elequ2 1179	. . . . . . . . . 10 |- (w = y -> (x e. w <-> x e. y))
2	1	anbi1d 628	. . . . . . . . 9 |- (w = y -> ((x e. w /\ A.yph) <-> (x e. y /\ A.yph)))
3	2	exbidv 1321	. . . . . . . 8 |- (w = y -> (E.x(x e. w /\ A.yph) <-> E.x(x e. y /\ A.yph)))
4	3	bibi2d 629	. . . . . . 7 |- (w = y -> ((z e. x <-> E.x(x e. w /\ A.yph)) <-> (z e. x <-> E.x(x e. y /\ A.yph))))
5	4	albidv 1320	. . . . . 6 |- (w = y -> (A.z(z e. x <-> E.x(x e. w /\ A.yph)) <-> A.z(z e. x <-> E.x(x e. y /\ A.yph))))
6	5	exbidv 1321	. . . . 5 |- (w = y -> (E.xA.z(z e. x <-> E.x(x e. w /\ A.yph)) <-> E.xA.z(z e. x <-> E.x(x e. y /\ A.yph))))
7	6	imbi2d 623	. . . 4 |- (w = y -> ((A.xE.yA.z(ph -> z = y) -> E.xA.z(z e. x <-> E.x(x e. w /\ A.yph))) <-> (A.xE.yA.z(ph -> z = y) -> E.xA.z(z e. x <-> E.x(x e. y /\ A.yph)))))
8		ax-4 1014	. . . . . . . . . 10 |- (A.yph -> ph)
9	8	imim1i 16	. . . . . . . . 9 |- ((ph -> z = y) -> (A.yph -> z = y))
10	9	19.20i 1033	. . . . . . . 8 |- (A.z(ph -> z = y) -> A.z(A.yph -> z = y))
11	10	19.22i 1081	. . . . . . 7 |- (E.yA.z(ph -> z = y) -> E.yA.z(A.yph -> z = y))
12	11	19.20i 1033	. . . . . 6 |- (A.xE.yA.z(ph -> z = y) -> A.xE.yA.z(A.yph -> z = y))
13		ax-rep 2748	. . . . . 6 |- (A.xE.yA.z(A.yph -> z = y) -> E.yA.z(z e. y <-> E.x(x e. w /\ A.yph)))
14	12, 13	syl 10	. . . . 5 |- (A.xE.yA.z(ph -> z = y) -> E.yA.z(z e. y <-> E.x(x e. w /\ A.yph)))
15		ax-17 1012	. . . . . . . 8 |- (z e. y -> A.x z e. y)
16		hbe1 1057	. . . . . . . 8 |- (E.x(x e. w /\ A.yph) -> A.xE.x(x e. w /\ A.yph))
17	15, 16	hbbi 1051	. . . . . . 7 |- ((z e. y <-> E.x(x e. w /\ A.yph)) -> A.x(z e. y <-> E.x(x e. w /\ A.yph)))
18	17	hbal 1046	. . . . . 6 |- (A.z(z e. y <-> E.x(x e. w /\ A.yph)) -> A.xA.z(z e. y <-> E.x(x e. w /\ A.yph)))
19		ax-17 1012	. . . . . . . 8 |- (z e. x -> A.y z e. x)
20		ax-17 1012	. . . . . . . . . 10 |- (x e. w -> A.y x e. w)
21		hba1 1044	. . . . . . . . . 10 |- (A.yph -> A.yA.yph)
22	20, 21	hban 1050	. . . . . . . . 9 |- ((x e. w /\ A.yph) -> A.y(x e. w /\ A.yph))
23	22	hbex 1047	. . . . . . . 8 |- (E.x(x e. w /\ A.yph) -> A.yE.x(x e. w /\ A.yph))
24	19, 23	hbbi 1051	. . . . . . 7 |- ((z e. x <-> E.x(x e. w /\ A.yph)) -> A.y(z e. x <-> E.x(x e. w /\ A.yph)))
25	24	hbal 1046	. . . . . 6 |- (A.z(z e. x <-> E.x(x e. w /\ A.yph)) -> A.yA.z(z e. x <-> E.x(x e. w /\ A.yph)))
26		elequ2 1179	. . . . . . . 8 |- (y = x -> (z e. y <-> z e. x))
27	26	bibi1d 630	. . . . . . 7 |- (y = x -> ((z e. y <-> E.x(x e. w /\ A.yph)) <-> (z e. x <-> E.x(x e. w /\ A.yph))))
28	27	albidv 1320	. . . . . 6 |- (y = x -> (A.z(z e. y <-> E.x(x e. w /\ A.yph)) <-> A.z(z e. x <-> E.x(x e. w /\ A.yph))))
29	18, 25, 28	cbvex 1208	. . . . 5 |- (E.yA.z(z e. y <-> E.x(x e. w /\ A.yph)) <-> E.xA.z(z e. x <-> E.x(x e. w /\ A.yph)))
30	14, 29	sylib 205	. . . 4 |- (A.xE.yA.z(ph -> z = y) -> E.xA.z(z e. x <-> E.x(x e. w /\ A.yph)))
31	7, 30	chvarv 1369	. . 3 |- (A.xE.yA.z(ph -> z = y) -> E.xA.z(z e. x <-> E.x(x e. y /\ A.yph)))
32	31	19.35ri 1118	. 2 |- E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph)))
33		ax-17 1012	. . . . . . . . 9 |- (ph -> A.yph)
34	33	19.3 1072	. . . . . . . 8 |- (A.yph <-> ph)
35	34	anbi2i 491	. . . . . . 7 |- ((x e. y /\ A.yph) <-> (x e. y /\ ph))
36	35	exbii 1092	. . . . . 6 |- (E.x(x e. y /\ A.yph) <-> E.x(x e. y /\ ph))
37	36	bibi2i 619	. . . . 5 |- ((z e. x <-> E.x(x e. y /\ A.yph)) <-> (z e. x <-> E.x(x e. y /\ ph)))
38	37	albii 1040	. . . 4 |- (A.z(z e. x <-> E.x(x e. y /\ A.yph)) <-> A.z(z e. x <-> E.x(x e. y /\ ph)))
39	38	imbi2i 192	. . 3 |- ((E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph))) <-> (E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ ph))))
40	39	exbii 1092	. 2 |- (E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph))) <-> E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ ph))))
41	32, 40	mpbi 196	1 |- E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ ph)))

Syntax hints:   -> wi 3   <-> wb 153   /\ wa 230  A.wal 995   = wceq 997   e. wcel 999  E.wex 1021

This theorem is referenced by:  axrep2 2750

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-12 1009  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-rep 2748

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022

Copyright terms: Public domain