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

Theorem equvini 1987
Description: A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require z to be distinct from x and y (making the proof longer). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Assertion
Ref Expression
equvini (x = yz(x = z z = y))

Proof of Theorem equvini
StepHypRef Expression
1 equcomi 1679 . . . . . 6 (z = xx = z)
21alimi 1559 . . . . 5 (z z = xz x = z)
3 a9e 1951 . . . . 5 z z = y
42, 3jctir 524 . . . 4 (z z = x → (z x = z z z = y))
54a1d 22 . . 3 (z z = x → (x = y → (z x = z z z = y)))
6 19.29 1596 . . 3 ((z x = z z z = y) → z(x = z z = y))
75, 6syl6 29 . 2 (z z = x → (x = yz(x = z z = y)))
8 a9e 1951 . . . . . 6 z z = x
91eximi 1576 . . . . . 6 (z z = xz x = z)
108, 9ax-mp 5 . . . . 5 z x = z
11102a1i 24 . . . 4 (z z = y → (x = yz x = z))
1211anc2ri 541 . . 3 (z z = y → (x = y → (z x = z z z = y)))
13 19.29r 1597 . . 3 ((z x = z z z = y) → z(x = z z = y))
1412, 13syl6 29 . 2 (z z = y → (x = yz(x = z z = y)))
15 ioran 476 . . 3 (¬ (z z = x z z = y) ↔ (¬ z z = x ¬ z z = y))
16 nfeqf 1958 . . . 4 ((¬ z z = x ¬ z z = y) → Ⅎz x = y)
17 ax-8 1675 . . . . . 6 (x = z → (x = yz = y))
1817anc2li 540 . . . . 5 (x = z → (x = y → (x = z z = y)))
1918equcoms 1681 . . . 4 (z = x → (x = y → (x = z z = y)))
2016, 19spimed 1977 . . 3 ((¬ z z = x ¬ z z = y) → (x = yz(x = z z = y)))
2115, 20sylbi 187 . 2 (¬ (z z = x z z = y) → (x = yz(x = z z = y)))
227, 14, 21ecase3 907 1 (x = yz(x = z z = y))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wo 357   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
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545
This theorem is referenced by:  equvin  2001  sbequi  2059
  Copyright terms: Public domain W3C validator