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

Theorem elequ2 1730
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 1729 . 2  |-  ( x  =  y  ->  (
z  e.  x  -> 
z  e.  y ) )
2 ax-14 1729 . . 3  |-  ( y  =  x  ->  (
z  e.  y  -> 
z  e.  x ) )
32equcoms 1693 . 2  |-  ( x  =  y  ->  (
z  e.  y  -> 
z  e.  x ) )
41, 3impbid 184 1  |-  ( x  =  y  ->  (
z  e.  x  <->  z  e.  y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  ax11wdemo  1738  dveel2  2100  elsb4  2180  dveel2ALT  2268  ax11el  2271  axext3  2419  axext4  2420  bm1.1  2421  axrep1  4314  axrep2  4315  axrep3  4316  axrep4  4317  bm1.3ii  4326  nalset  4333  zfun  4695  fv3  5737  tz7.48lem  6691  aceq0  7992  dfac2a  8003  axdc3lem2  8324  zfac  8333  nd2  8456  nd3  8457  axrepndlem2  8461  axunndlem1  8463  axunnd  8464  axpowndlem2  8466  axpowndlem3  8467  axpowndlem4  8468  axpownd  8469  axregndlem2  8471  axregnd  8472  axinfndlem1  8473  axacndlem5  8479  zfcndrep  8482  zfcndun  8483  zfcndac  8487  axgroth4  8700  nqereu  8799  rpnnen  12819  neiptopnei  17189  2ndc1stc  17507  kqt0lem  17761  regr1lem2  17765  nrmr0reg  17774  hauspwpwf1  18012  dya2iocuni  24626  erdsze  24881  untsucf  25152  untangtr  25156  dfon2lem3  25405  dfon2lem6  25408  dfon2lem7  25409  dfon2lem8  25410  dfon2  25412  axext4dist  25421  distel  25424  axextndbi  25425  fness  26354  fneref  26356  prtlem13  26709  prtlem15  26716  prtlem17  26717  aomclem8  27128  ax10ext  27575  dveel2NEW7  29404  elsb4NEW7  29542
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator