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

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

Proof of Theorem elequ1
StepHypRef Expression
1 ax8 1910 . 2  |-  ( x  =  y  ->  (
x  e.  z  -> 
y  e.  z ) )
2 ax8 1910 . . 3  |-  ( y  =  x  ->  (
y  e.  z  ->  x  e.  z )
)
32equcoms 1872 . 2  |-  ( x  =  y  ->  (
y  e.  z  ->  x  e.  z )
)
41, 3impbid 195 1  |-  ( x  =  y  ->  (
x  e.  z  <->  y  e.  z ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672
This theorem is referenced by:  cleljust  1912  ax12wdemo  1926  cleljustALT  2102  cleljustALT2  2103  dveel1  2219  axc14  2221  elsb3  2283  axsep  4517  nalset  4533  zfpow  4580  zfun  6603  tz7.48lem  7176  unxpdomlem1  7794  pssnn  7808  zfinf  8162  aceq0  8567  dfac3  8570  dfac5lem2  8573  dfac5lem3  8574  dfac2a  8578  zfac  8908  nd1  9030  axextnd  9034  axrepndlem1  9035  axrepndlem2  9036  axunndlem1  9038  axunnd  9039  axpowndlem2  9041  axpowndlem3  9042  axpowndlem4  9043  axregndlem1  9045  axregnd  9047  zfcndun  9058  zfcndpow  9059  zfcndinf  9061  zfcndac  9062  fpwwe2lem12  9084  axgroth3  9274  axgroth4  9275  nqereu  9372  rpnnen  14356  mdetunilem9  19722  madugsum  19745  neiptopnei  20225  2ndc1stc  20543  nrmr0reg  20841  alexsubALTlem4  21143  xrsmopn  21908  itg2cn  22800  itgcn  22879  sqff1o  24188  dya2iocuni  29178  bnj849  29808  erdsze  29997  untsucf  30409  untangtr  30413  dfon2lem3  30502  dfon2lem6  30505  dfon2lem7  30506  dfon2  30509  axextdist  30517  distel  30521  neibastop2lem  31087  bj-elequ12  31343  bj-axsep  31474  bj-nalset  31475  bj-zfpow  31476  bj-ru0  31607  prtlem5  32494  ax12el  32577  pw2f1ocnv  35963  aomclem8  35990  lcosslsp  40739
  Copyright terms: Public domain W3C validator