Theorem axrep1 2662

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 2661 -> axrep1 2662 -> axrep2 2663 -> axrepnd 4869 -> zfcndrep 4889 = ax-rep 2661.

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 1124	. . . . . . . . . 10 |- (w = y -> (x e. w <-> x e. y))
2	1	anbi1d 615	. . . . . . . . 9 |- (w = y -> ((x e. w /\ A.yph) <-> (x e. y /\ A.yph)))
3	2	exbidv 1261	. . . . . . . 8 |- (w = y -> (E.x(x e. w /\ A.yph) <-> E.x(x e. y /\ A.yph)))
4	3	bibi2d 616	. . . . . . 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 1260	. . . . . 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 1261	. . . . 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 610	. . . 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 951	. . . . . . . . . 10 |- (A.yph -> ph)
9	8	imim1i 16	. . . . . . . . 9 |- ((ph -> z = y) -> (A.yph -> z = y))
10	9	19.20i 968	. . . . . . . 8 |- (A.z(ph -> z = y) -> A.z(A.yph -> z = y))
11	10	19.22i 1016	. . . . . . 7 |- (E.yA.z(ph -> z = y) -> E.yA.z(A.yph -> z = y))
12	11	19.20i 968	. . . . . 6 |- (A.xE.yA.z(ph -> z = y) -> A.xE.yA.z(A.yph -> z = y))
13		ax-rep 2661	. . . . . 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 1190	. . . . . . . 8 |- (z e. y -> A.x z e. y)
16		hbe1 990	. . . . . . . 8 |- (E.x(x e. w /\ A.yph) -> A.xE.x(x e. w /\ A.yph))
17	15, 16	hbbi 986	. . . . . . 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 981	. . . . . 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 1190	. . . . . . . 8 |- (z e. x -> A.y z e. x)
20		ax-17 1190	. . . . . . . . . 10 |- (x e. w -> A.y x e. w)
21		hba1 979	. . . . . . . . . 10 |- (A.yph -> A.yA.yph)
22	20, 21	hban 985	. . . . . . . . 9 |- ((x e. w /\ A.yph) -> A.y(x e. w /\ A.yph))
23	22	hbex 982	. . . . . . . 8 |- (E.x(x e. w /\ A.yph) -> A.yE.x(x e. w /\ A.yph))
24	19, 23	hbbi 986	. . . . . . 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 981	. . . . . 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 1124	. . . . . . . 8 |- (y = x -> (z e. y <-> z e. x))
27	26	bibi1d 617	. . . . . . 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 1260	. . . . . 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 1149	. . . . 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 198	. . . 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 1309	. . 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 1053	. 2 |- E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph)))
33		ax-17 1190	. . . . . . . . 9 |- (ph -> A.yph)
34	33	19.3 1007	. . . . . . . 8 |- (A.yph <-> ph)
35	34	anbi2i 479	. . . . . . 7 |- ((x e. y /\ A.yph) <-> (x e. y /\ ph))
36	35	exbii 1027	. . . . . 6 |- (E.x(x e. y /\ A.yph) <-> E.x(x e. y /\ ph))
37	36	bibi2i 606	. . . . 5 |- ((z e. x <-> E.x(x e. y /\ A.yph)) <-> (z e. x <-> E.x(x e. y /\ ph)))
38	37	albii 975	. . . 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 185	. . 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 1027	. 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 189	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 146   /\ wa 223  A.wal 950  E.wex 956   = wceq 1099   e. wcel 1105

This theorem is referenced by:  axrep2 2663

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-12 1104  ax-14 1108  ax-17 1190  ax-rep 2661

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957

Copyright terms: Public domain