MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elequ2 Structured version   Visualization version   GIF version

Theorem elequ2 2122
Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
elequ2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))

Proof of Theorem elequ2
StepHypRef Expression
1 ax9 2121 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax9 2121 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 2024 . 2 (𝑥 = 𝑦 → (𝑧𝑦𝑧𝑥))
41, 3impbid 211 1 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by:  elequ2g  2123  elsb2  2124  ax12wdemo  2132  dveel2  2461  axextg  2710  axextmo  2712  eleq2w  2822  nfcvf  2937  unissb  4905  dftr2c  5230  axrep1  5248  axreplem  5249  axrep4  5252  axsepg  5262  bm1.3ii  5264  nalset  5275  fv3  6865  zfun  7678  tz7.48lem  8392  coflton  8622  aceq1  10060  aceq0  10061  aceq2  10062  dfac2a  10072  kmlem4  10096  axdc3lem2  10394  zfac  10403  nd2  10531  nd3  10532  axrepndlem2  10536  axunndlem1  10538  axunnd  10539  axpowndlem2  10541  axpowndlem3  10542  axpowndlem4  10543  axpownd  10544  axregndlem2  10546  axregnd  10547  axinfndlem1  10548  axacndlem5  10554  zfcndrep  10557  zfcndun  10558  zfcndac  10562  axgroth4  10775  nqereu  10872  mdetunilem9  21985  neiptopnei  22499  2ndc1stc  22818  restlly  22850  kqt0lem  23103  regr1lem2  23107  nrmr0reg  23116  hauspwpwf1  23354  dya2iocuni  32923  erdsze  33836  untsucf  34321  untangtr  34325  dfon2lem3  34399  dfon2lem6  34402  dfon2lem7  34403  dfon2lem8  34404  dfon2  34406  axextbdist  34414  distel  34417  axextndbi  34418  fness  34850  fneref  34851  bj-elequ12  35172  bj-axc14nf  35350  bj-bm1.3ii  35564  matunitlindflem1  36103  prtlem13  37359  prtlem15  37366  prtlem17  37367  dveel2ALT  37430  ax12el  37433  aomclem8  41417  unielss  41581  elintima  41999  mnuprdlem3  42628  ismnushort  42655  axc11next  42760  setcthin  47149
  Copyright terms: Public domain W3C validator