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

Theorem elequ1 1728
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 1727 . 2  |-  ( x  =  y  ->  (
x  e.  z  -> 
y  e.  z ) )
2 ax-13 1727 . . 3  |-  ( y  =  x  ->  (
y  e.  z  ->  x  e.  z )
)
32equcoms 1693 . 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  1738  cleljust  2103  cleljustALT  2104  dveel1  2105  ax15  2107  elsb3  2179  ax11el  2271  axsep  4329  nalset  4340  zfpow  4378  zfun  4702  tz7.48lem  6698  unxpdomlem1  7313  pssnn  7327  zfinf  7594  aceq0  7999  dfac3  8002  dfac5lem2  8005  dfac5lem3  8006  dfac2a  8010  zfac  8340  nd1  8462  axextnd  8466  axrepndlem1  8467  axrepndlem2  8468  axunndlem1  8470  axunnd  8471  axpowndlem2  8473  axpowndlem3  8474  axpowndlem4  8475  axregndlem1  8477  axregnd  8479  zfcndun  8490  zfcndpow  8491  zfcndinf  8493  zfcndac  8494  fpwwe2lem12  8516  axgroth3  8706  axgroth4  8707  nqereu  8806  rpnnen  12826  neiptopnei  17196  2ndc1stc  17514  nrmr0reg  17781  alexsubALTlem4  18081  xrsmopn  18843  itg2cn  19655  itgcn  19734  sqff1o  20965  dya2iocuni  24633  erdsze  24888  untsucf  25159  untangtr  25163  dfon2lem3  25412  dfon2lem6  25415  dfon2lem7  25416  dfon2  25419  axextdist  25427  distel  25431  neibastop2lem  26389  prtlem5  26705  pw2f1ocnv  27108  aomclem8  27136  bnj849  29296  dveel1NEW7  29465  ax15NEW7  29536  elsb3NEW7  29603  cleljustNEW7  29627
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-13 1727
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator