Theorem elequ2 1872

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

Step	Hyp	Ref	Expression
1		ax-9 1871	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax-9 1871	. . 3 |- ( y = x -> ( z e. y -> z e. x ) )
3	2	equcoms 1844	. 2 |- ( x = y -> ( z e. y -> z e. x ) )
4	1, 3	impbid 193	1 |- ( x = y -> ( z e. x <-> z e. y ) )

Syntax hints:   -> wi 4   <-> wb 187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871

This theorem depends on definitions:  df-bi 188  df-ex 1660

This theorem is referenced by:  ax12wdemo  1880  dveel2  2163  elsb4  2228  axext3  2400  axext3OLD  2401  axext4  2402  bm1.1  2403  bm1.1OLD  2404  axrep1  4530  axrep2  4531  axrep3  4532  axrep4  4533  bm1.3ii  4542  nalset  4553  fv3  5885  zfun  6589  tz7.48lem  7157  aceq0  8538  dfac2a  8549  axdc3lem2  8870  zfac  8879  nd2  9002  nd3  9003  axrepndlem2  9007  axunndlem1  9009  axunnd  9010  axpowndlem2  9012  axpowndlem3  9013  axpowndlem4  9014  axpownd  9015  axregndlem2  9017  axregnd  9018  axinfndlem1  9019  axacndlem5  9025  zfcndrep  9028  zfcndun  9029  zfcndac  9033  axgroth4  9246  nqereu  9343  rpnnen  14246  mdetunilem9  19569  neiptopnei  20072  2ndc1stc  20390  kqt0lem  20675  regr1lem2  20679  nrmr0reg  20688  hauspwpwf1  20926  dya2iocuni  28941  erdsze  29710  untsucf  30122  untangtr  30126  dfon2lem3  30215  dfon2lem6  30218  dfon2lem7  30219  dfon2lem8  30220  dfon2  30222  axext4dist  30231  distel  30234  axextndbi  30235  fness  30787  fneref  30788  bj-elequ2g  31014  bj-elequ12  31016  bj-axext3  31131  bj-axrep1  31151  bj-axrep2  31152  bj-axrep3  31153  bj-axrep4  31154  bj-nalset  31157  bj-eleq2w  31204  bj-axsep2  31275  prtlem13  32148  prtlem15  32155  prtlem17  32156  dveel2ALT  32219  ax12el  32222  aomclem8  35629  elintima  35888  axc11next  36398