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

Theorem elequ2 2130
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 2129 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax9 2129 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 2028 . 2 (𝑥 = 𝑦 → (𝑧𝑦𝑧𝑥))
41, 3impbid 215 1 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782
This theorem is referenced by:  elsb4  2131  elequ2g  2132  ax12wdemo  2140  dveel2  2487  axextg  2798  axextmo  2800  eleq2w  2899  nfcvf  3008  axrep1  5178  axreplem  5179  axrep4  5182  axsepg  5191  bm1.3ii  5193  nalset  5204  fv3  6681  zfun  7458  tz7.48lem  8075  aceq1  9543  aceq0  9544  aceq2  9545  dfac2a  9555  kmlem4  9579  axdc3lem2  9873  zfac  9882  nd2  10010  nd3  10011  axrepndlem2  10015  axunndlem1  10017  axunnd  10018  axpowndlem2  10020  axpowndlem3  10021  axpowndlem4  10022  axpownd  10023  axregndlem2  10025  axregnd  10026  axinfndlem1  10027  axacndlem5  10033  zfcndrep  10036  zfcndun  10037  zfcndac  10041  axgroth4  10254  nqereu  10351  elnpi  10410  mdetunilem9  21234  neiptopnei  21746  2ndc1stc  22065  restlly  22097  kqt0lem  22350  regr1lem2  22354  nrmr0reg  22363  hauspwpwf1  22601  dya2iocuni  31626  erdsze  32534  untsucf  33021  untangtr  33025  dfon2lem3  33115  dfon2lem6  33118  dfon2lem7  33119  dfon2lem8  33120  dfon2  33122  axextbdist  33130  distel  33133  axextndbi  33134  fness  33782  fneref  33783  bj-elequ12  34097  bj-axc14nf  34266  bj-bm1.3ii  34453  matunitlindflem1  35025  prtlem13  36136  prtlem15  36143  prtlem17  36144  dveel2ALT  36207  ax12el  36210  aomclem8  39949  elintima  40298  mnuprdlem3  40930  axc11next  41058
  Copyright terms: Public domain W3C validator