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

Theorem elequ1 1687
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 1686 . 2  |-  ( x  =  y  ->  (
x  e.  z  -> 
y  e.  z ) )
2 ax-13 1686 . . 3  |-  ( y  =  x  ->  (
y  e.  z  ->  x  e.  z )
)
32equcoms 1651 . 2  |-  ( x  =  y  ->  (
y  e.  z  ->  x  e.  z )
)
41, 3impbid 183 1  |-  ( x  =  y  ->  (
x  e.  z  <->  y  e.  z ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  ax11wdemo  1697  cleljust  1954  cleljustALT  1955  dveel1  1959  ax15  1961  elsb3  2042  ax11el  2133  axsep  4140  nalset  4151  zfpow  4189  zfun  4513  tz7.48lem  6453  unxpdomlem1  7067  pssnn  7081  zfinf  7340  aceq0  7745  dfac3  7748  dfac5lem2  7751  dfac5lem3  7752  dfac2a  7756  zfac  8086  nd1  8209  axextnd  8213  axrepndlem1  8214  axrepndlem2  8215  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axregndlem1  8224  axregnd  8226  zfcndun  8237  zfcndpow  8238  zfcndinf  8240  zfcndac  8241  fpwwe2lem12  8263  axgroth3  8453  axgroth4  8454  nqereu  8553  rpnnen  12505  2ndc1stc  17177  nrmr0reg  17440  alexsubALTlem4  17744  xrsmopn  18318  itg2cn  19118  itgcn  19197  sqff1o  20420  erdsze  23733  untsucf  24056  untangtr  24060  dfon2lem3  24141  dfon2lem6  24144  dfon2lem7  24145  dfon2  24148  axextdist  24156  distel  24160  neibastop2lem  26309  prtlem5  26722  pw2f1ocnv  27130  aomclem8  27159
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-13 1686
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator