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

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

Proof of Theorem elequ2
StepHypRef Expression
1 ax-9 1823 . 2  |-  ( x  =  y  ->  (
z  e.  x  -> 
z  e.  y ) )
2 ax-9 1823 . . 3  |-  ( y  =  x  ->  (
z  e.  y  -> 
z  e.  x ) )
32equcoms 1796 . 2  |-  ( x  =  y  ->  (
z  e.  y  -> 
z  e.  x ) )
41, 3impbid 191 1  |-  ( x  =  y  ->  (
z  e.  x  <->  z  e.  y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823
This theorem depends on definitions:  df-bi 185  df-ex 1614
This theorem is referenced by:  ax12wdemo  1832  dveel2  2113  elsb4  2180  dveel2ALT  2270  ax12el  2273  axext3  2437  axext3OLD  2438  axext4  2439  bm1.1  2440  bm1.1OLD  2441  axrep1  4569  axrep2  4570  axrep3  4571  axrep4  4572  bm1.3ii  4581  nalset  4593  fv3  5885  zfun  6592  tz7.48lem  7124  aceq0  8516  dfac2a  8527  axdc3lem2  8848  zfac  8857  nd2  8980  nd3  8981  axrepndlem2  8985  axunndlem1  8987  axunnd  8988  axpowndlem2  8990  axpowndlem2OLD  8991  axpowndlem3  8992  axpowndlem3OLD  8993  axpowndlem4  8994  axpownd  8995  axregndlem2  8997  axregnd  8998  axregndOLD  8999  axinfndlem1  9000  axacndlem5  9006  zfcndrep  9009  zfcndun  9010  zfcndac  9014  axgroth4  9227  nqereu  9324  rpnnen  13972  mdetunilem9  19249  neiptopnei  19760  2ndc1stc  20078  kqt0lem  20363  regr1lem2  20367  nrmr0reg  20376  hauspwpwf1  20614  dya2iocuni  28427  erdsze  28843  untsucf  29300  untangtr  29304  dfon2lem3  29434  dfon2lem6  29437  dfon2lem7  29438  dfon2lem8  29439  dfon2  29441  axext4dist  29450  distel  29453  axextndbi  29454  fness  30372  fneref  30373  prtlem13  30814  prtlem15  30821  prtlem17  30822  aomclem8  31211  axc11next  31517  bj-elequ2g  34380  bj-elequ12  34382  bj-axext3  34497  bj-axrep1  34517  bj-axrep2  34518  bj-axrep3  34519  bj-axrep4  34520  bj-nalset  34523  bj-eleq2w  34566  bj-axsep2  34636  elintima  37925
  Copyright terms: Public domain W3C validator