Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  equvini Unicode version

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

Proof of Theorem equvini
StepHypRef Expression
1 equcomi 1822 . . . . . 6
21alimi 1546 . . . . 5
3 a9e 1817 . . . . 5
42, 3jctir 526 . . . 4
54a1d 24 . . 3
6 19.29 1595 . . 3
75, 6syl6 31 . 2
8 a9e 1817 . . . . . 6
91eximi 1574 . . . . . 6
108, 9ax-mp 10 . . . . 5
1110a1ii 26 . . . 4
1211anc2ri 543 . . 3
13 19.29r 1596 . . 3
1412, 13syl6 31 . 2
15 ioran 478 . . 3
16 nfeqf 1849 . . . 4
17 ax-8 1623 . . . . . 6
1817anc2li 542 . . . . 5
1918equcoms 1825 . . . 4
2016, 19a4imed 1870 . . 3
2115, 20sylbi 189 . 2
227, 14, 21ecase3 912 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6   wo 359   wa 360  wal 1532  wex 1537   wceq 1619 This theorem is referenced by:  sbequi  1952  equvin  2000  a12lem2  28298 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540
 Copyright terms: Public domain W3C validator