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

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

Proof of Theorem elequ1
StepHypRef Expression
1 ax-13 1723 . 2  |-  ( x  =  y  ->  (
x  e.  z  -> 
y  e.  z ) )
2 ax-13 1723 . . 3  |-  ( y  =  x  ->  (
y  e.  z  ->  x  e.  z )
)
32equcoms 1689 . 2  |-  ( x  =  y  ->  (
y  e.  z  ->  x  e.  z )
)
41, 3impbid 184 1  |-  ( x  =  y  ->  (
x  e.  z  <->  y  e.  z ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  ax11wdemo  1734  cleljust  2064  cleljustALT  2065  dveel1  2068  ax15  2070  elsb3  2152  ax11el  2244  axsep  4289  nalset  4300  zfpow  4338  zfun  4661  tz7.48lem  6657  unxpdomlem1  7272  pssnn  7286  zfinf  7550  aceq0  7955  dfac3  7958  dfac5lem2  7961  dfac5lem3  7962  dfac2a  7966  zfac  8296  nd1  8418  axextnd  8422  axrepndlem1  8423  axrepndlem2  8424  axunndlem1  8426  axunnd  8427  axpowndlem2  8429  axpowndlem3  8430  axpowndlem4  8431  axregndlem1  8433  axregnd  8435  zfcndun  8446  zfcndpow  8447  zfcndinf  8449  zfcndac  8450  fpwwe2lem12  8472  axgroth3  8662  axgroth4  8663  nqereu  8762  rpnnen  12781  neiptopnei  17151  2ndc1stc  17467  nrmr0reg  17734  alexsubALTlem4  18034  xrsmopn  18796  itg2cn  19608  itgcn  19687  sqff1o  20918  dya2iocuni  24586  erdsze  24841  untsucf  25112  untangtr  25116  dfon2lem3  25355  dfon2lem6  25358  dfon2lem7  25359  dfon2  25362  axextdist  25370  distel  25374  neibastop2lem  26279  prtlem5  26595  pw2f1ocnv  26998  aomclem8  27027  bnj849  29002  dveel1NEW7  29171  ax15NEW7  29240  elsb3NEW7  29304  cleljustNEW7  29328
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 1662  ax-8 1683  ax-13 1723
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator