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

Theorem elequ2 1722
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 1721 . 2  |-  ( x  =  y  ->  (
z  e.  x  -> 
z  e.  y ) )
2 ax-14 1721 . . 3  |-  ( y  =  x  ->  (
z  e.  y  -> 
z  e.  x ) )
32equcoms 1688 . 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  1730  dveel2  2046  elsb4  2130  dveel2ALT  2218  ax11el  2221  axext3  2363  axext4  2364  bm1.1  2365  axrep1  4255  axrep2  4256  axrep3  4257  axrep4  4258  bm1.3ii  4267  nalset  4274  zfun  4635  fv3  5677  tz7.48lem  6627  aceq0  7925  dfac2a  7936  axdc3lem2  8257  zfac  8266  nd2  8389  nd3  8390  axrepndlem2  8394  axunndlem1  8396  axunnd  8397  axpowndlem2  8399  axpowndlem3  8400  axpowndlem4  8401  axpownd  8402  axregndlem2  8404  axregnd  8405  axinfndlem1  8406  axacndlem5  8412  zfcndrep  8415  zfcndun  8416  zfcndac  8420  axgroth4  8633  nqereu  8732  rpnnen  12746  neiptopnei  17112  2ndc1stc  17428  kqt0lem  17682  regr1lem2  17686  nrmr0reg  17695  hauspwpwf1  17933  dya2iocuni  24420  erdsze  24660  untsucf  24931  untangtr  24935  dfon2lem3  25158  dfon2lem6  25161  dfon2lem7  25162  dfon2lem8  25163  dfon2  25165  axext4dist  25174  distel  25177  axextndbi  25178  fness  26046  fneref  26048  prtlem13  26401  prtlem15  26408  prtlem17  26409  aomclem8  26821  ax10ext  27268  dveel2NEW7  28797  elsb4NEW7  28930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator