Theorem axrep1 2694

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 2693 -> axrep1 2694 -> axrep2 2695 -> axrepnd 4946 -> zfcndrep 4966 = ax-rep 2693.

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 1137	. . . . . . . . . 10 |- (w = y -> (x e. w <-> x e. y))
2	1	anbi1d 617	. . . . . . . . 9 |- (w = y -> ((x e. w /\ A.yph) <-> (x e. y /\ A.yph)))
3	2	exbidv 1279	. . . . . . . 8 |- (w = y -> (E.x(x e. w /\ A.yph) <-> E.x(x e. y /\ A.yph)))
4	3	bibi2d 618	. . . . . . 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 1278	. . . . . 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 1279	. . . . 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 612	. . . 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 973	. . . . . . . . . 10 |- (A.yph -> ph)
9	8	imim1i 16	. . . . . . . . 9 |- ((ph -> z = y) -> (A.yph -> z = y))
10	9	19.20i 992	. . . . . . . 8 |- (A.z(ph -> z = y) -> A.z(A.yph -> z = y))
11	10	19.22i 1040	. . . . . . 7 |- (E.yA.z(ph -> z = y) -> E.yA.z(A.yph -> z = y))
12	11	19.20i 992	. . . . . 6 |- (A.xE.yA.z(ph -> z = y) -> A.xE.yA.z(A.yph -> z = y))
13		ax-rep 2693	. . . . . 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 971	. . . . . . . 8 |- (z e. y -> A.x z e. y)
16		hbe1 1016	. . . . . . . 8 |- (E.x(x e. w /\ A.yph) -> A.xE.x(x e. w /\ A.yph))
17	15, 16	hbbi 1010	. . . . . . 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 1005	. . . . . 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 971	. . . . . . . 8 |- (z e. x -> A.y z e. x)
20		ax-17 971	. . . . . . . . . 10 |- (x e. w -> A.y x e. w)
21		hba1 1003	. . . . . . . . . 10 |- (A.yph -> A.yA.yph)
22	20, 21	hban 1009	. . . . . . . . 9 |- ((x e. w /\ A.yph) -> A.y(x e. w /\ A.yph))
23	22	hbex 1006	. . . . . . . 8 |- (E.x(x e. w /\ A.yph) -> A.yE.x(x e. w /\ A.yph))
24	19, 23	hbbi 1010	. . . . . . 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 1005	. . . . . 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 1137	. . . . . . . 8 |- (y = x -> (z e. y <-> z e. x))
27	26	bibi1d 619	. . . . . . 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 1278	. . . . . 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 1166	. . . . 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 1327	. . 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 1077	. 2 |- E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph)))
33		ax-17 971	. . . . . . . . 9 |- (ph -> A.yph)
34	33	19.3 1031	. . . . . . . 8 |- (A.yph <-> ph)
35	34	anbi2i 480	. . . . . . 7 |- ((x e. y /\ A.yph) <-> (x e. y /\ ph))
36	35	exbii 1051	. . . . . 6 |- (E.x(x e. y /\ A.yph) <-> E.x(x e. y /\ ph))
37	36	bibi2i 608	. . . . 5 |- ((z e. x <-> E.x(x e. y /\ A.yph)) <-> (z e. x <-> E.x(x e. y /\ ph)))
38	37	albii 999	. . . 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 1051	. 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 954   = wceq 956   e. wcel 958  E.wex 980

This theorem is referenced by:  axrep2 2695

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-rep 2693

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

Copyright terms: Public domain