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

Theorem elequ2 2002
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 2001 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax9 2001 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 1945 . 2 (𝑥 = 𝑦 → (𝑧𝑦𝑧𝑥))
41, 3impbid 202 1 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703
This theorem is referenced by:  ax12wdemo  2010  dveel2  2369  elsb4  2433  axext3  2602  axext3ALT  2603  axext4  2604  bm1.1  2605  eleq2w  2683  axrep1  4763  axrep2  4764  axrep3  4765  axrep4  4766  axsep2  4773  bm1.3ii  4775  nalset  4786  fv3  6193  zfun  6935  tz7.48lem  7521  aceq1  8925  aceq0  8926  aceq2  8927  dfac2a  8937  kmlem4  8960  axdc3lem2  9258  zfac  9267  nd2  9395  nd3  9396  axrepndlem2  9400  axunndlem1  9402  axunnd  9403  axpowndlem2  9405  axpowndlem3  9406  axpowndlem4  9407  axpownd  9408  axregndlem2  9410  axregnd  9411  axinfndlem1  9412  axacndlem5  9418  zfcndrep  9421  zfcndun  9422  zfcndac  9426  axgroth4  9639  nqereu  9736  mdetunilem9  20407  neiptopnei  20917  2ndc1stc  21235  restlly  21267  kqt0lem  21520  regr1lem2  21524  nrmr0reg  21533  hauspwpwf1  21772  dya2iocuni  30319  erdsze  31158  untsucf  31561  untangtr  31565  dfon2lem3  31664  dfon2lem6  31667  dfon2lem7  31668  dfon2lem8  31669  dfon2  31671  axext4dist  31680  distel  31683  axextndbi  31684  fness  32319  fneref  32320  bj-elequ2g  32641  bj-elequ12  32643  bj-axext3  32744  bj-axrep1  32763  bj-axrep2  32764  bj-axrep3  32765  bj-axrep4  32766  bj-nalset  32769  bj-axc14nf  32813  bj-axsep2  32896  matunitlindflem1  33376  prtlem13  33972  prtlem15  33979  prtlem17  33980  dveel2ALT  34043  ax12el  34046  aomclem8  37450  elintima  37764  axc11next  38427
  Copyright terms: Public domain W3C validator