HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem axrepndlem2 6097
Description: Lemma for the Axiom of Replacement with no distinct variable conditions.
Assertion
Ref Expression
axrepndlem2 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph))))
Proof of Theorem axrepndlem2
StepHypRef Expression
1 hbnae 1507 . . . . 5 |- (-. A.x x = y -> A.x -. A.x x = y)
2 hbnae 1507 . . . . 5 |- (-. A.x x = z -> A.x -. A.x x = z)
31, 2hban 1356 . . . 4 |- ((-. A.x x = y /\ -. A.x x = z) -> A.x(-. A.x x = y /\ -. A.x x = z))
4 hbnae 1507 . . . . . . 7 |- (-. A.x x = y -> A.y -. A.x x = y)
5 hbnae 1507 . . . . . . 7 |- (-. A.x x = z -> A.y -. A.x x = z)
64, 5hban 1356 . . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> A.y(-. A.x x = y /\ -. A.x x = z))
7 hbnae 1507 . . . . . . . 8 |- (-. A.x x = y -> A.z -. A.x x = y)
8 hbnae 1507 . . . . . . . 8 |- (-. A.x x = z -> A.z -. A.x x = z)
97, 8hban 1356 . . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> A.z(-. A.x x = y /\ -. A.x x = z))
10 ax-17 1317 . . . . . . . . . 10 |- (ph -> A.wph)
1110hbsb3 1575 . . . . . . . . 9 |- ([w / x]ph -> A.x[w / x]ph)
1211a1i 8 . . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> ([w / x]ph -> A.x[w / x]ph))
13 ax-12 1310 . . . . . . . . 9 |- (-. A.x x = z -> (-. A.x x = y -> (z = y -> A.x z = y)))
1413impcom 378 . . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (z = y -> A.x z = y))
153, 12, 14hbimd 1468 . . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (([w / x]ph -> z = y) -> A.x([w / x]ph -> z = y)))
169, 15hbald 1471 . . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.z([w / x]ph -> z = y) -> A.xA.z([w / x]ph -> z = y)))
176, 16hbexd 1472 . . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.yA.z([w / x]ph -> z = y) -> A.xE.yA.z([w / x]ph -> z = y)))
18 dveel1 1747 . . . . . . . 8 |- (-. A.x x = z -> (z e. w -> A.x z e. w))
1918adantl 424 . . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (z e. w -> A.x z e. w))
20 ax-17 1317 . . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
21 dveel2 1748 . . . . . . . . . 10 |- (-. A.x x = y -> (w e. y -> A.x w e. y))
2221adantr 425 . . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. y -> A.x w e. y))
236, 12hbald 1471 . . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y[w / x]ph -> A.xA.y[w / x]ph))
2422, 23hband 1469 . . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> ((w e. y /\ A.y[w / x]ph) -> A.x(w e. y /\ A.y[w / x]ph)))
2520, 24hbexd 1472 . . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.w(w e. y /\ A.y[w / x]ph) -> A.xE.w(w e. y /\ A.y[w / x]ph)))
263, 19, 25hbbid 1470 . . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> ((z e. w <-> E.w(w e. y /\ A.y[w / x]ph)) -> A.x(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))))
279, 26hbald 1471 . . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph)) -> A.xA.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))))
283, 17, 27hbimd 1468 . . . 4 |- ((-. A.x x = y /\ -. A.x x = z) -> ((E.yA.z([w / x]ph -> z = y) -> A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))) -> A.x(E.yA.z([w / x]ph -> z = y) -> A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph)))))
29 nd5 6094 . . . . . . . . 9 |- (-. A.x x = y -> (w = x -> A.y w = x))
3029adantr 425 . . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.y w = x))
3130imdistani 491 . . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
32 hba1 1350 . . . . . . . . 9 |- (A.y w = x -> A.yA.y w = x)
336, 32hban 1356 . . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> A.y((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
34 nd5 6094 . . . . . . . . . . 11 |- (-. A.x x = z -> (w = x -> A.z w = x))
3534imdistani 491 . . . . . . . . . 10 |- ((-. A.x x = z /\ w = x) -> (-. A.x x = z /\ A.z w = x))
36 hba1 1350 . . . . . . . . . . . 12 |- (A.z w = x -> A.zA.z w = x)
378, 36hban 1356 . . . . . . . . . . 11 |- ((-. A.x x = z /\ A.z w = x) -> A.z(-. A.x x = z /\ A.z w = x))
38 sbequ12r 1546 . . . . . . . . . . . . . 14 |- (w = x -> ([w / x]ph <-> ph))
3938imbi1d 675 . . . . . . . . . . . . 13 |- (w = x -> (([w / x]ph -> z = y) <-> (ph -> z = y)))
4039a4s 1330 . . . . . . . . . . . 12 |- (A.z w = x -> (([w / x]ph -> z = y) <-> (ph -> z = y)))
4140adantl 424 . . . . . . . . . . 11 |- ((-. A.x x = z /\ A.z w = x) -> (([w / x]ph -> z = y) <-> (ph -> z = y)))
4237, 41albid 1459 . . . . . . . . . 10 |- ((-. A.x x = z /\ A.z w = x) -> (A.z([w / x]ph -> z = y) <-> A.z(ph -> z = y)))
4335, 42syl 12 . . . . . . . . 9 |- ((-. A.x x = z /\ w = x) -> (A.z([w / x]ph -> z = y) <-> A.z(ph -> z = y)))
44 simpr 350 . . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> -. A.x x = z)
45 ax-4 1319 . . . . . . . . 9 |- (A.y w = x -> w = x)
4643, 44, 45syl2an 503 . . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> (A.z([w / x]ph -> z = y) <-> A.z(ph -> z = y)))
4733, 46exbid 1460 . . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> (E.yA.z([w / x]ph -> z = y) <-> E.yA.z(ph -> z = y)))
4831, 47syl 12 . . . . . 6 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (E.yA.z([w / x]ph -> z = y) <-> E.yA.z(ph -> z = y)))
4934adantl 424 . . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.z w = x))
5049imdistani 491 . . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((-. A.x x = y /\ -. A.x x = z) /\ A.z w = x))
519, 36hban 1356 . . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.z w = x) -> A.z((-. A.x x = y /\ -. A.x x = z) /\ A.z w = x))
52 elequ2 1497 . . . . . . . . . . 11 |- (w = x -> (z e. w <-> z e. x))
5352adantl 424 . . . . . . . . . 10 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (z e. w <-> z e. x))
54 elequ1 1496 . . . . . . . . . . . . . . 15 |- (w = x -> (w e. y <-> x e. y))
5554adantl 424 . . . . . . . . . . . . . 14 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (w e. y <-> x e. y))
56 sbal2 1749 . . . . . . . . . . . . . . . . . 18 |- (-. A.y y = x -> ([w / x]A.yph <-> A.y[w / x]ph))
5756nalequcoms 1504 . . . . . . . . . . . . . . . . 17 |- (-. A.x x = y -> ([w / x]A.yph <-> A.y[w / x]ph))
5857bicomd 580 . . . . . . . . . . . . . . . 16 |- (-. A.x x = y -> (A.y[w / x]ph <-> [w / x]A.yph))
59 sbequ12r 1546 . . . . . . . . . . . . . . . 16 |- (w = x -> ([w / x]A.yph <-> A.yph))
6058, 59sylan9bb 599 . . . . . . . . . . . . . . 15 |- ((-. A.x x = y /\ w = x) -> (A.y[w / x]ph <-> A.yph))
6160adantlr 429 . . . . . . . . . . . . . 14 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (A.y[w / x]ph <-> A.yph))
6255, 61anbi12d 690 . . . . . . . . . . . . 13 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((w e. y /\ A.y[w / x]ph) <-> (x e. y /\ A.yph)))
6362ex 402 . . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> ((w e. y /\ A.y[w / x]ph) <-> (x e. y /\ A.yph))))
643, 24, 63cbvexd 1704 . . . . . . . . . . 11 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.w(w e. y /\ A.y[w / x]ph) <-> E.x(x e. y /\ A.yph)))
6564adantr 425 . . . . . . . . . 10 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (E.w(w e. y /\ A.y[w / x]ph) <-> E.x(x e. y /\ A.yph)))
6653, 65bibi12d 691 . . . . . . . . 9 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((z e. w <-> E.w(w e. y /\ A.y[w / x]ph)) <-> (z e. x <-> E.x(x e. y /\ A.yph))))
67 ax-4 1319 . . . . . . . . 9 |- (A.z w = x -> w = x)
6866, 67sylan2 500 . . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.z w = x) -> ((z e. w <-> E.w(w e. y /\ A.y[w / x]ph)) <-> (z e. x <-> E.x(x e. y /\ A.yph))))
6951, 68albid 1459 . . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.z w = x) -> (A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph)) <-> A.z(z e. x <-> E.x(x e. y /\ A.yph))))
7050, 69syl 12 . . . . . 6 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph)) <-> A.z(z e. x <-> E.x(x e. y /\ A.yph))))
7148, 70imbi12d 688 . . . . 5 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((E.yA.z([w / x]ph -> z = y) -> A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))) <-> (E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph)))))
7271ex 402 . . . 4 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> ((E.yA.z([w / x]ph -> z = y) -> A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))) <-> (E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph))))))
733, 28, 72cbvexd 1704 . . 3 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.w(E.yA.z([w / x]ph -> z = y) -> A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))) <-> E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph)))))
74 axrepndlem1 6096 . . 3 |- (-. A.y y = z -> E.w(E.yA.z([w / x]ph -> z = y) -> A.z(z e. w <-> E.w(w e. y /\ A.y[w / x]ph))))
7573, 74syl5bi 225 . 2 |- ((-. A.x x = y /\ -. A.x x = z) -> (-. A.y y = z -> E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph)))))
7675imp 377 1 |- (((-. A.x x = y /\ -. A.x x = z) /\ -. A.y y = z) -> E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph))))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  [wsbc 1534
This theorem is referenced by:  axrepnd 6098
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-rep 3428
This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536
Copyright terms: Public domain