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

Theorem elequ2 1767
Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
elequ2  |-  ( x  =  y  ->  (
z  e.  x  <->  z  e.  y ) )

Proof of Theorem elequ2
StepHypRef Expression
1 ax-9 1766 . 2  |-  ( x  =  y  ->  (
z  e.  x  -> 
z  e.  y ) )
2 ax-9 1766 . . 3  |-  ( y  =  x  ->  (
z  e.  y  -> 
z  e.  x ) )
32equcoms 1739 . 2  |-  ( x  =  y  ->  (
z  e.  y  -> 
z  e.  x ) )
41, 3impbid 191 1  |-  ( x  =  y  ->  (
z  e.  x  <->  z  e.  y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766
This theorem depends on definitions:  df-bi 185  df-ex 1592
This theorem is referenced by:  ax12wdemo  1775  dveel2  2080  elsb4  2157  dveel2ALT  2257  ax12el  2260  axext3  2442  axext3OLD  2443  axext4  2444  bm1.1  2445  bm1.1OLD  2446  axrep1  4554  axrep2  4555  axrep3  4556  axrep4  4557  bm1.3ii  4566  nalset  4579  fv3  5872  zfun  6570  tz7.48lem  7098  aceq0  8490  dfac2a  8501  axdc3lem2  8822  zfac  8831  nd2  8954  nd3  8955  axrepndlem2  8959  axunndlem1  8961  axunnd  8962  axpowndlem2  8964  axpowndlem2OLD  8965  axpowndlem3  8966  axpowndlem3OLD  8967  axpowndlem4  8968  axpownd  8969  axregndlem2  8971  axregnd  8972  axregndOLD  8973  axinfndlem1  8974  axacndlem5  8980  zfcndrep  8983  zfcndun  8984  zfcndac  8988  axgroth4  9201  nqereu  9298  rpnnen  13812  mdetunilem9  18884  neiptopnei  19394  2ndc1stc  19713  kqt0lem  19967  regr1lem2  19971  nrmr0reg  19980  hauspwpwf1  20218  dya2iocuni  27882  erdsze  28274  untsucf  28545  untangtr  28549  dfon2lem3  28782  dfon2lem6  28785  dfon2lem7  28786  dfon2lem8  28787  dfon2  28789  axext4dist  28798  distel  28801  axextndbi  28802  fness  29743  fneref  29745  prtlem13  30202  prtlem15  30209  prtlem17  30210  aomclem8  30602  axc11next  30848  bj-elequ2g  33196  bj-elequ12  33198  bj-axext3  33312  bj-axrep1  33332  bj-axrep2  33333  bj-axrep3  33334  bj-axrep4  33335  bj-nalset  33338  bj-eleq2w  33381  bj-axsep2  33451
  Copyright terms: Public domain W3C validator