NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax11el GIF version

Theorem ax11el 2194
Description: Basis step for constructing a substitution instance of ax-11o 2141 without using ax-11o 2141. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax11el x x = y → (x = y → (z wx(x = yz w))))

Proof of Theorem ax11el
Dummy variables u v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 19.26 1593 . . 3 (x(x = z x = w) ↔ (x x = z x x = w))
2 elequ1 1713 . . . . . . . . 9 (x = y → (x xy x))
3 elequ2 1715 . . . . . . . . 9 (x = y → (y xy y))
42, 3bitrd 244 . . . . . . . 8 (x = y → (x xy y))
54adantl 452 . . . . . . 7 ((¬ x x = y x = y) → (x xy y))
6 ax-17 1616 . . . . . . . . . 10 (v vx v v)
7 ax-17 1616 . . . . . . . . . 10 (y yv y y)
8 elequ1 1713 . . . . . . . . . . 11 (v = y → (v vy v))
9 elequ2 1715 . . . . . . . . . . 11 (v = y → (y vy y))
108, 9bitrd 244 . . . . . . . . . 10 (v = y → (v vy y))
116, 7, 10dvelimf-o 2180 . . . . . . . . 9 x x = y → (y yx y y))
124biimprcd 216 . . . . . . . . . 10 (y y → (x = yx x))
1312alimi 1559 . . . . . . . . 9 (x y yx(x = yx x))
1411, 13syl6 29 . . . . . . . 8 x x = y → (y yx(x = yx x)))
1514adantr 451 . . . . . . 7 ((¬ x x = y x = y) → (y yx(x = yx x)))
165, 15sylbid 206 . . . . . 6 ((¬ x x = y x = y) → (x xx(x = yx x)))
1716adantl 452 . . . . 5 ((x(x = z x = w) x x = y x = y)) → (x xx(x = yx x)))
18 elequ1 1713 . . . . . . . . 9 (x = z → (x xz x))
19 elequ2 1715 . . . . . . . . 9 (x = w → (z xz w))
2018, 19sylan9bb 680 . . . . . . . 8 ((x = z x = w) → (x xz w))
2120sps-o 2159 . . . . . . 7 (x(x = z x = w) → (x xz w))
22 nfa1-o 2166 . . . . . . . 8 xx(x = z x = w)
2321imbi2d 307 . . . . . . . 8 (x(x = z x = w) → ((x = yx x) ↔ (x = yz w)))
2422, 23albid 1772 . . . . . . 7 (x(x = z x = w) → (x(x = yx x) ↔ x(x = yz w)))
2521, 24imbi12d 311 . . . . . 6 (x(x = z x = w) → ((x xx(x = yx x)) ↔ (z wx(x = yz w))))
2625adantr 451 . . . . 5 ((x(x = z x = w) x x = y x = y)) → ((x xx(x = yx x)) ↔ (z wx(x = yz w))))
2717, 26mpbid 201 . . . 4 ((x(x = z x = w) x x = y x = y)) → (z wx(x = yz w)))
2827exp32 588 . . 3 (x(x = z x = w) → (¬ x x = y → (x = y → (z wx(x = yz w)))))
291, 28sylbir 204 . 2 ((x x = z x x = w) → (¬ x x = y → (x = y → (z wx(x = yz w)))))
30 elequ1 1713 . . . . . . 7 (x = y → (x wy w))
3130ad2antll 709 . . . . . 6 ((¬ x x = w x x = y x = y)) → (x wy w))
32 ax-15 2143 . . . . . . . . 9 x x = y → (¬ x x = w → (y wx y w)))
3332impcom 419 . . . . . . . 8 ((¬ x x = w ¬ x x = y) → (y wx y w))
3433adantrr 697 . . . . . . 7 ((¬ x x = w x x = y x = y)) → (y wx y w))
3530biimprcd 216 . . . . . . . 8 (y w → (x = yx w))
3635alimi 1559 . . . . . . 7 (x y wx(x = yx w))
3734, 36syl6 29 . . . . . 6 ((¬ x x = w x x = y x = y)) → (y wx(x = yx w)))
3831, 37sylbid 206 . . . . 5 ((¬ x x = w x x = y x = y)) → (x wx(x = yx w)))
3938adantll 694 . . . 4 (((x x = z ¬ x x = w) x x = y x = y)) → (x wx(x = yx w)))
40 elequ1 1713 . . . . . . 7 (x = z → (x wz w))
4140sps-o 2159 . . . . . 6 (x x = z → (x wz w))
4241imbi2d 307 . . . . . . 7 (x x = z → ((x = yx w) ↔ (x = yz w)))
4342dral2-o 2181 . . . . . 6 (x x = z → (x(x = yx w) ↔ x(x = yz w)))
4441, 43imbi12d 311 . . . . 5 (x x = z → ((x wx(x = yx w)) ↔ (z wx(x = yz w))))
4544ad2antrr 706 . . . 4 (((x x = z ¬ x x = w) x x = y x = y)) → ((x wx(x = yx w)) ↔ (z wx(x = yz w))))
4639, 45mpbid 201 . . 3 (((x x = z ¬ x x = w) x x = y x = y)) → (z wx(x = yz w)))
4746exp32 588 . 2 ((x x = z ¬ x x = w) → (¬ x x = y → (x = y → (z wx(x = yz w)))))
48 elequ2 1715 . . . . . . 7 (x = y → (z xz y))
4948ad2antll 709 . . . . . 6 ((¬ x x = z x x = y x = y)) → (z xz y))
50 ax-15 2143 . . . . . . . . 9 x x = z → (¬ x x = y → (z yx z y)))
5150imp 418 . . . . . . . 8 ((¬ x x = z ¬ x x = y) → (z yx z y))
5251adantrr 697 . . . . . . 7 ((¬ x x = z x x = y x = y)) → (z yx z y))
5348biimprcd 216 . . . . . . . 8 (z y → (x = yz x))
5453alimi 1559 . . . . . . 7 (x z yx(x = yz x))
5552, 54syl6 29 . . . . . 6 ((¬ x x = z x x = y x = y)) → (z yx(x = yz x)))
5649, 55sylbid 206 . . . . 5 ((¬ x x = z x x = y x = y)) → (z xx(x = yz x)))
5756adantlr 695 . . . 4 (((¬ x x = z x x = w) x x = y x = y)) → (z xx(x = yz x)))
5819sps-o 2159 . . . . . 6 (x x = w → (z xz w))
5958imbi2d 307 . . . . . . 7 (x x = w → ((x = yz x) ↔ (x = yz w)))
6059dral2-o 2181 . . . . . 6 (x x = w → (x(x = yz x) ↔ x(x = yz w)))
6158, 60imbi12d 311 . . . . 5 (x x = w → ((z xx(x = yz x)) ↔ (z wx(x = yz w))))
6261ad2antlr 707 . . . 4 (((¬ x x = z x x = w) x x = y x = y)) → ((z xx(x = yz x)) ↔ (z wx(x = yz w))))
6357, 62mpbid 201 . . 3 (((¬ x x = z x x = w) x x = y x = y)) → (z wx(x = yz w)))
6463exp32 588 . 2 ((¬ x x = z x x = w) → (¬ x x = y → (x = y → (z wx(x = yz w)))))
65 a9ev 1656 . . . . 5 u u = w
66 a9ev 1656 . . . . . . 7 v v = z
67 ax-1 6 . . . . . . . . . . 11 (v u → (x = yv u))
6867alrimiv 1631 . . . . . . . . . 10 (v ux(x = yv u))
69 elequ1 1713 . . . . . . . . . . . . 13 (v = z → (v uz u))
70 elequ2 1715 . . . . . . . . . . . . 13 (u = w → (z uz w))
7169, 70sylan9bb 680 . . . . . . . . . . . 12 ((v = z u = w) → (v uz w))
7271adantl 452 . . . . . . . . . . 11 (((¬ x x = z ¬ x x = w) (v = z u = w)) → (v uz w))
73 dveeq2-o 2184 . . . . . . . . . . . . . . 15 x x = z → (v = zx v = z))
74 dveeq2-o 2184 . . . . . . . . . . . . . . 15 x x = w → (u = wx u = w))
7573, 74im2anan9 808 . . . . . . . . . . . . . 14 ((¬ x x = z ¬ x x = w) → ((v = z u = w) → (x v = z x u = w)))
7675imp 418 . . . . . . . . . . . . 13 (((¬ x x = z ¬ x x = w) (v = z u = w)) → (x v = z x u = w))
77 19.26 1593 . . . . . . . . . . . . 13 (x(v = z u = w) ↔ (x v = z x u = w))
7876, 77sylibr 203 . . . . . . . . . . . 12 (((¬ x x = z ¬ x x = w) (v = z u = w)) → x(v = z u = w))
79 nfa1-o 2166 . . . . . . . . . . . . 13 xx(v = z u = w)
8071sps-o 2159 . . . . . . . . . . . . . 14 (x(v = z u = w) → (v uz w))
8180imbi2d 307 . . . . . . . . . . . . 13 (x(v = z u = w) → ((x = yv u) ↔ (x = yz w)))
8279, 81albid 1772 . . . . . . . . . . . 12 (x(v = z u = w) → (x(x = yv u) ↔ x(x = yz w)))
8378, 82syl 15 . . . . . . . . . . 11 (((¬ x x = z ¬ x x = w) (v = z u = w)) → (x(x = yv u) ↔ x(x = yz w)))
8472, 83imbi12d 311 . . . . . . . . . 10 (((¬ x x = z ¬ x x = w) (v = z u = w)) → ((v ux(x = yv u)) ↔ (z wx(x = yz w))))
8568, 84mpbii 202 . . . . . . . . 9 (((¬ x x = z ¬ x x = w) (v = z u = w)) → (z wx(x = yz w)))
8685exp32 588 . . . . . . . 8 ((¬ x x = z ¬ x x = w) → (v = z → (u = w → (z wx(x = yz w)))))
8786exlimdv 1636 . . . . . . 7 ((¬ x x = z ¬ x x = w) → (v v = z → (u = w → (z wx(x = yz w)))))
8866, 87mpi 16 . . . . . 6 ((¬ x x = z ¬ x x = w) → (u = w → (z wx(x = yz w))))
8988exlimdv 1636 . . . . 5 ((¬ x x = z ¬ x x = w) → (u u = w → (z wx(x = yz w))))
9065, 89mpi 16 . . . 4 ((¬ x x = z ¬ x x = w) → (z wx(x = yz w)))
9190a1d 22 . . 3 ((¬ x x = z ¬ x x = w) → (x = y → (z wx(x = yz w))))
9291a1d 22 . 2 ((¬ x x = z ¬ x x = w) → (¬ x x = y → (x = y → (z wx(x = yz w)))))
9329, 47, 64, 924cases 915 1 x x = y → (x = y → (z wx(x = yz w))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wa 358  wal 1540  wex 1541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-4 2135  ax-5o 2136  ax-6o 2137  ax-10o 2139  ax-12o 2142  ax-15 2143
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator