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

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

Proof of Theorem elequ2
StepHypRef Expression
1 ax-14 1688 . 2  |-  ( x  =  y  ->  (
z  e.  x  -> 
z  e.  y ) )
2 ax-14 1688 . . 3  |-  ( y  =  x  ->  (
z  e.  y  -> 
z  e.  x ) )
32equcoms 1651 . 2  |-  ( x  =  y  ->  (
z  e.  y  -> 
z  e.  x ) )
41, 3impbid 183 1  |-  ( x  =  y  ->  (
z  e.  x  <->  z  e.  y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  ax11wdemo  1697  dveel2  1960  elsb4  2043  dveel2ALT  2130  ax11el  2133  axext3  2266  axext4  2267  bm1.1  2268  axrep1  4132  axrep2  4133  axrep3  4134  axrep4  4135  bm1.3ii  4144  nalset  4151  zfun  4513  fv3  5541  tz7.48lem  6453  aceq0  7745  dfac2a  7756  axdc3lem2  8077  zfac  8086  nd2  8210  nd3  8211  axrepndlem2  8215  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axpownd  8223  axregndlem2  8225  axregnd  8226  axinfndlem1  8227  axacndlem5  8233  zfcndrep  8236  zfcndun  8237  zfcndac  8241  axgroth4  8454  nqereu  8553  rpnnen  12505  2ndc1stc  17177  regr1lem2  17431  nrmr0reg  17440  hauspwpwf1  17682  erdsze  23733  untsucf  24056  untangtr  24060  dfon2lem3  24141  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  dfon2  24148  axext4dist  24157  distel  24160  axextndbi  24161  basexre  25522  fness  26282  fneref  26284  prtlem13  26736  prtlem15  26743  prtlem17  26744  aomclem8  27159  ax10ext  27606
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator