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

Theorem elequ2 1701
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 1700 . 2  |-  ( x  =  y  ->  (
z  e.  x  -> 
z  e.  y ) )
2 ax-14 1700 . . 3  |-  ( y  =  x  ->  (
z  e.  y  -> 
z  e.  x ) )
32equcoms 1666 . 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  1709  dveel2  1973  elsb4  2056  dveel2ALT  2143  ax11el  2146  axext3  2279  axext4  2280  bm1.1  2281  axrep1  4148  axrep2  4149  axrep3  4150  axrep4  4151  bm1.3ii  4160  nalset  4167  zfun  4529  fv3  5557  tz7.48lem  6469  aceq0  7761  dfac2a  7772  axdc3lem2  8093  zfac  8102  nd2  8226  nd3  8227  axrepndlem2  8231  axunndlem1  8233  axunnd  8234  axpowndlem2  8236  axpowndlem3  8237  axpowndlem4  8238  axpownd  8239  axregndlem2  8241  axregnd  8242  axinfndlem1  8243  axacndlem5  8249  zfcndrep  8252  zfcndun  8253  zfcndac  8257  axgroth4  8470  nqereu  8569  rpnnen  12521  2ndc1stc  17193  regr1lem2  17447  nrmr0reg  17456  hauspwpwf1  17698  erdsze  23748  untsucf  24071  untangtr  24075  dfon2lem3  24212  dfon2lem6  24215  dfon2lem7  24216  dfon2lem8  24217  dfon2  24219  axext4dist  24228  distel  24231  axextndbi  24232  basexre  25625  fness  26385  fneref  26387  prtlem13  26839  prtlem15  26846  prtlem17  26847  aomclem8  27262  ax10ext  27709  dveel2NEW7  29443  elsb4NEW7  29576
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator