Theorem axrep1 2684

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 2683 -> axrep1 2684 -> axrep2 2685 -> axrepnd 4918 -> zfcndrep 4938 = ax-rep 2683.

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 1133	. . . . . . . . . 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 1274	. . . . . . . 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 1273	. . . . . 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 1274	. . . . 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 970	. . . . . . . . . 10 |- (A.yph -> ph)
9	8	imim1i 16	. . . . . . . . 9 |- ((ph -> z = y) -> (A.yph -> z = y))
10	9	19.20i 989	. . . . . . . 8 |- (A.z(ph -> z = y) -> A.z(A.yph -> z = y))
11	10	19.22i 1036	. . . . . . 7 |- (E.yA.z(ph -> z = y) -> E.yA.z(A.yph -> z = y))
12	11	19.20i 989	. . . . . 6 |- (A.xE.yA.z(ph -> z = y) -> A.xE.yA.z(A.yph -> z = y))
13		ax-rep 2683	. . . . . 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 968	. . . . . . . 8 |- (z e. y -> A.x z e. y)
16		hbe1 1012	. . . . . . . 8 |- (E.x(x e. w /\ A.yph) -> A.xE.x(x e. w /\ A.yph))
17	15, 16	hbbi 1007	. . . . . . 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 1002	. . . . . 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 968	. . . . . . . 8 |- (z e. x -> A.y z e. x)
20		ax-17 968	. . . . . . . . . 10 |- (x e. w -> A.y x e. w)
21		hba1 1000	. . . . . . . . . 10 |- (A.yph -> A.yA.yph)
22	20, 21	hban 1006	. . . . . . . . 9 |- ((x e. w /\ A.yph) -> A.y(x e. w /\ A.yph))
23	22	hbex 1003	. . . . . . . 8 |- (E.x(x e. w /\ A.yph) -> A.yE.x(x e. w /\ A.yph))
24	19, 23	hbbi 1007	. . . . . . 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 1002	. . . . . 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 1133	. . . . . . . 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 1273	. . . . . 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 1162	. . . . 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 1322	. . 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 1073	. 2 |- E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph)))
33		ax-17 968	. . . . . . . . 9 |- (ph -> A.yph)
34	33	19.3 1027	. . . . . . . 8 |- (A.yph <-> ph)
35	34	anbi2i 479	. . . . . . 7 |- ((x e. y /\ A.yph) <-> (x e. y /\ ph))
36	35	exbii 1047	. . . . . 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 996	. . . 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 1047	. 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 951   = wceq 953   e. wcel 955  E.wex 977

This theorem is referenced by:  axrep2 2685

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-rep 2683

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

Copyright terms: Public domain