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

Theorem ax12olem1 1927
Description: Lemma for ax12o 1934. Similar to equvin 2001 but with a negated equality. (Contributed by NM, 24-Dec-2015.)
Assertion
Ref Expression
ax12olem1 (w(y = w ¬ z = w) ↔ ¬ y = z)
Distinct variable groups:   y,w   z,w

Proof of Theorem ax12olem1
StepHypRef Expression
1 ax-8 1675 . . . . 5 (y = w → (y = zw = z))
2 equcomi 1679 . . . . 5 (w = zz = w)
31, 2syl6 29 . . . 4 (y = w → (y = zz = w))
43con3and 428 . . 3 ((y = w ¬ z = w) → ¬ y = z)
54exlimiv 1634 . 2 (w(y = w ¬ z = w) → ¬ y = z)
6 ax-17 1616 . . 3 y = zw ¬ y = z)
7 ax-8 1675 . . . . . . . 8 (w = z → (w = yz = y))
8 equcomi 1679 . . . . . . . 8 (z = yy = z)
97, 8syl6 29 . . . . . . 7 (w = z → (w = yy = z))
109equcoms 1681 . . . . . 6 (z = w → (w = yy = z))
1110com12 27 . . . . 5 (w = y → (z = wy = z))
1211con3d 125 . . . 4 (w = y → (¬ y = z → ¬ z = w))
13 equcomi 1679 . . . 4 (w = yy = w)
1412, 13jctild 527 . . 3 (w = y → (¬ y = z → (y = w ¬ z = w)))
156, 14spimeh 1667 . 2 y = zw(y = w ¬ z = w))
165, 15impbii 180 1 (w(y = w ¬ z = w) ↔ ¬ y = z)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wa 358  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
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542
This theorem is referenced by:  ax12olem2  1928
  Copyright terms: Public domain W3C validator