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

Theorem elequ1 1713
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 1712 . 2  |-  ( x  =  y  ->  (
x  e.  z  -> 
y  e.  z ) )
2 ax-13 1712 . . 3  |-  ( y  =  x  ->  (
y  e.  z  ->  x  e.  z )
)
32equcoms 1681 . 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  1723  cleljust  2019  cleljustALT  2020  dveel1  2024  ax15  2026  elsb3  2108  ax11el  2199  axsep  4221  nalset  4232  zfpow  4270  zfun  4595  tz7.48lem  6540  unxpdomlem1  7155  pssnn  7169  zfinf  7430  aceq0  7835  dfac3  7838  dfac5lem2  7841  dfac5lem3  7842  dfac2a  7846  zfac  8176  nd1  8299  axextnd  8303  axrepndlem1  8304  axrepndlem2  8305  axunndlem1  8307  axunnd  8308  axpowndlem2  8310  axpowndlem3  8311  axpowndlem4  8312  axregndlem1  8314  axregnd  8316  zfcndun  8327  zfcndpow  8328  zfcndinf  8330  zfcndac  8331  fpwwe2lem12  8353  axgroth3  8543  axgroth4  8544  nqereu  8643  rpnnen  12602  2ndc1stc  17283  nrmr0reg  17546  alexsubALTlem4  17846  xrsmopn  18420  itg2cn  19222  itgcn  19301  sqff1o  20532  neiptopnei  23445  dya2iocuni  23897  erdsze  24137  untsucf  24460  untangtr  24464  dfon2lem3  24699  dfon2lem6  24702  dfon2lem7  24703  dfon2  24706  axextdist  24714  distel  24718  neibastop2lem  25633  prtlem5  26045  pw2f1ocnv  26453  aomclem8  26482  dveel1NEW7  28888  ax15NEW7  28957  elsb3NEW7  29021  cleljustNEW7  29045  cleljustALTNEW7  29046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712
This theorem depends on definitions:  df-bi 177  df-ex 1542
  Copyright terms: Public domain W3C validator