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

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

Proof of Theorem ax11eq
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 equid 1676 . . . . . . . 8 x = x
32a1i 10 . . . . . . 7 (x = yx = x)
43ax-gen 1546 . . . . . 6 x(x = yx = x)
54a1i 10 . . . . 5 (x = xx(x = yx = x))
6 equequ1 1684 . . . . . . . . 9 (x = z → (x = xz = x))
7 equequ2 1686 . . . . . . . . 9 (x = w → (z = xz = w))
86, 7sylan9bb 680 . . . . . . . 8 ((x = z x = w) → (x = xz = w))
98sps-o 2159 . . . . . . 7 (x(x = z x = w) → (x = xz = w))
10 nfa1-o 2166 . . . . . . . 8 xx(x = z x = w)
119imbi2d 307 . . . . . . . 8 (x(x = z x = w) → ((x = yx = x) ↔ (x = yz = w)))
1210, 11albid 1772 . . . . . . 7 (x(x = z x = w) → (x(x = yx = x) ↔ x(x = yz = w)))
139, 12imbi12d 311 . . . . . 6 (x(x = z x = w) → ((x = xx(x = yx = x)) ↔ (z = wx(x = yz = w))))
1413adantr 451 . . . . 5 ((x(x = z x = w) x x = y x = y)) → ((x = xx(x = yx = x)) ↔ (z = wx(x = yz = w))))
155, 14mpbii 202 . . . 4 ((x(x = z x = w) x x = y x = y)) → (z = wx(x = yz = w)))
1615exp32 588 . . 3 (x(x = z x = w) → (¬ x x = y → (x = y → (z = wx(x = yz = w)))))
171, 16sylbir 204 . 2 ((x x = z x x = w) → (¬ x x = y → (x = y → (z = wx(x = yz = w)))))
18 equequ1 1684 . . . . . . 7 (x = y → (x = wy = w))
1918ad2antll 709 . . . . . 6 ((¬ x x = w x x = y x = y)) → (x = wy = w))
20 ax12o 1934 . . . . . . . . 9 x x = y → (¬ x x = w → (y = wx y = w)))
2120impcom 419 . . . . . . . 8 ((¬ x x = w ¬ x x = y) → (y = wx y = w))
2221adantrr 697 . . . . . . 7 ((¬ x x = w x x = y x = y)) → (y = wx y = w))
23 equtrr 1683 . . . . . . . 8 (y = w → (x = yx = w))
2423alimi 1559 . . . . . . 7 (x y = wx(x = yx = w))
2522, 24syl6 29 . . . . . 6 ((¬ x x = w x x = y x = y)) → (y = wx(x = yx = w)))
2619, 25sylbid 206 . . . . 5 ((¬ x x = w x x = y x = y)) → (x = wx(x = yx = w)))
2726adantll 694 . . . 4 (((x x = z ¬ x x = w) x x = y x = y)) → (x = wx(x = yx = w)))
28 equequ1 1684 . . . . . . 7 (x = z → (x = wz = w))
2928sps-o 2159 . . . . . 6 (x x = z → (x = wz = w))
3029imbi2d 307 . . . . . . 7 (x x = z → ((x = yx = w) ↔ (x = yz = w)))
3130dral2-o 2181 . . . . . 6 (x x = z → (x(x = yx = w) ↔ x(x = yz = w)))
3229, 31imbi12d 311 . . . . 5 (x x = z → ((x = wx(x = yx = w)) ↔ (z = wx(x = yz = w))))
3332ad2antrr 706 . . . 4 (((x x = z ¬ x x = w) x x = y x = y)) → ((x = wx(x = yx = w)) ↔ (z = wx(x = yz = w))))
3427, 33mpbid 201 . . 3 (((x x = z ¬ x x = w) x x = y x = y)) → (z = wx(x = yz = w)))
3534exp32 588 . 2 ((x x = z ¬ x x = w) → (¬ x x = y → (x = y → (z = wx(x = yz = w)))))
36 equequ2 1686 . . . . . . 7 (x = y → (z = xz = y))
3736ad2antll 709 . . . . . 6 ((¬ x x = z x x = y x = y)) → (z = xz = y))
38 ax12o 1934 . . . . . . . . 9 x x = z → (¬ x x = y → (z = yx z = y)))
3938imp 418 . . . . . . . 8 ((¬ x x = z ¬ x x = y) → (z = yx z = y))
4039adantrr 697 . . . . . . 7 ((¬ x x = z x x = y x = y)) → (z = yx z = y))
4136biimprcd 216 . . . . . . . 8 (z = y → (x = yz = x))
4241alimi 1559 . . . . . . 7 (x z = yx(x = yz = x))
4340, 42syl6 29 . . . . . 6 ((¬ x x = z x x = y x = y)) → (z = yx(x = yz = x)))
4437, 43sylbid 206 . . . . 5 ((¬ x x = z x x = y x = y)) → (z = xx(x = yz = x)))
4544adantlr 695 . . . 4 (((¬ x x = z x x = w) x x = y x = y)) → (z = xx(x = yz = x)))
467sps-o 2159 . . . . . 6 (x x = w → (z = xz = w))
4746imbi2d 307 . . . . . . 7 (x x = w → ((x = yz = x) ↔ (x = yz = w)))
4847dral2-o 2181 . . . . . 6 (x x = w → (x(x = yz = x) ↔ x(x = yz = w)))
4946, 48imbi12d 311 . . . . 5 (x x = w → ((z = xx(x = yz = x)) ↔ (z = wx(x = yz = w))))
5049ad2antlr 707 . . . 4 (((¬ x x = z x x = w) x x = y x = y)) → ((z = xx(x = yz = x)) ↔ (z = wx(x = yz = w))))
5145, 50mpbid 201 . . 3 (((¬ x x = z x x = w) x x = y x = y)) → (z = wx(x = yz = w)))
5251exp32 588 . 2 ((¬ x x = z x x = w) → (¬ x x = y → (x = y → (z = wx(x = yz = w)))))
53 a9ev 1656 . . . . 5 u u = w
54 a9ev 1656 . . . . . . 7 v v = z
55 ax-1 6 . . . . . . . . . . 11 (v = u → (x = yv = u))
5655alrimiv 1631 . . . . . . . . . 10 (v = ux(x = yv = u))
57 equequ1 1684 . . . . . . . . . . . . 13 (v = z → (v = uz = u))
58 equequ2 1686 . . . . . . . . . . . . 13 (u = w → (z = uz = w))
5957, 58sylan9bb 680 . . . . . . . . . . . 12 ((v = z u = w) → (v = uz = w))
6059adantl 452 . . . . . . . . . . 11 (((¬ x x = z ¬ x x = w) (v = z u = w)) → (v = uz = w))
61 dveeq2-o 2184 . . . . . . . . . . . . . . 15 x x = z → (v = zx v = z))
62 dveeq2-o 2184 . . . . . . . . . . . . . . 15 x x = w → (u = wx u = w))
6361, 62im2anan9 808 . . . . . . . . . . . . . 14 ((¬ x x = z ¬ x x = w) → ((v = z u = w) → (x v = z x u = w)))
6463imp 418 . . . . . . . . . . . . 13 (((¬ x x = z ¬ x x = w) (v = z u = w)) → (x v = z x u = w))
65 19.26 1593 . . . . . . . . . . . . 13 (x(v = z u = w) ↔ (x v = z x u = w))
6664, 65sylibr 203 . . . . . . . . . . . 12 (((¬ x x = z ¬ x x = w) (v = z u = w)) → x(v = z u = w))
67 nfa1-o 2166 . . . . . . . . . . . . 13 xx(v = z u = w)
6859sps-o 2159 . . . . . . . . . . . . . 14 (x(v = z u = w) → (v = uz = w))
6968imbi2d 307 . . . . . . . . . . . . 13 (x(v = z u = w) → ((x = yv = u) ↔ (x = yz = w)))
7067, 69albid 1772 . . . . . . . . . . . 12 (x(v = z u = w) → (x(x = yv = u) ↔ x(x = yz = w)))
7166, 70syl 15 . . . . . . . . . . 11 (((¬ x x = z ¬ x x = w) (v = z u = w)) → (x(x = yv = u) ↔ x(x = yz = w)))
7260, 71imbi12d 311 . . . . . . . . . 10 (((¬ x x = z ¬ x x = w) (v = z u = w)) → ((v = ux(x = yv = u)) ↔ (z = wx(x = yz = w))))
7356, 72mpbii 202 . . . . . . . . 9 (((¬ x x = z ¬ x x = w) (v = z u = w)) → (z = wx(x = yz = w)))
7473exp32 588 . . . . . . . 8 ((¬ x x = z ¬ x x = w) → (v = z → (u = w → (z = wx(x = yz = w)))))
7574exlimdv 1636 . . . . . . 7 ((¬ x x = z ¬ x x = w) → (v v = z → (u = w → (z = wx(x = yz = w)))))
7654, 75mpi 16 . . . . . 6 ((¬ x x = z ¬ x x = w) → (u = w → (z = wx(x = yz = w))))
7776exlimdv 1636 . . . . 5 ((¬ x x = z ¬ x x = w) → (u u = w → (z = wx(x = yz = w))))
7853, 77mpi 16 . . . 4 ((¬ x x = z ¬ x x = w) → (z = wx(x = yz = w)))
7978a1d 22 . . 3 ((¬ x x = z ¬ x x = w) → (x = y → (z = wx(x = yz = w))))
8079a1d 22 . 2 ((¬ x x = z ¬ x x = w) → (¬ x x = y → (x = y → (z = wx(x = yz = w)))))
8117, 35, 52, 804cases 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-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
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