Theorem elequ2 1763

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 1762	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax-9 1762	. . 3 |- ( y = x -> ( z e. y -> z e. x ) )
3	2	equcoms 1735	. 2 |- ( x = y -> ( z e. y -> z e. x ) )
4	1, 3	impbid 191	1 |- ( x = y -> ( z e. x <-> z e. y ) )

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 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762

This theorem depends on definitions:  df-bi 185  df-ex 1588

This theorem is referenced by:  ax12wdemo  1771  dveel2  2069  elsb4  2147  dveel2ALT  2247  ax12el  2250  axext3  2432  axext4  2433  bm1.1  2434  bm1.1OLD  2435  axrep1  4504  axrep2  4505  axrep3  4506  axrep4  4507  bm1.3ii  4516  nalset  4529  fv3  5804  zfun  6475  tz7.48lem  6998  aceq0  8391  dfac2a  8402  axdc3lem2  8723  zfac  8732  nd2  8855  nd3  8856  axrepndlem2  8860  axunndlem1  8862  axunnd  8863  axpowndlem2  8865  axpowndlem2OLD  8866  axpowndlem3  8867  axpowndlem3OLD  8868  axpowndlem4  8869  axpownd  8870  axregndlem2  8872  axregnd  8873  axregndOLD  8874  axinfndlem1  8875  axacndlem5  8881  zfcndrep  8884  zfcndun  8885  zfcndac  8889  axgroth4  9102  nqereu  9201  rpnnen  13613  mdetunilem9  18544  neiptopnei  18854  2ndc1stc  19173  kqt0lem  19427  regr1lem2  19431  nrmr0reg  19440  hauspwpwf1  19678  dya2iocuni  26834  erdsze  27226  untsucf  27497  untangtr  27501  dfon2lem3  27734  dfon2lem6  27737  dfon2lem7  27738  dfon2lem8  27739  dfon2  27741  axext4dist  27750  distel  27753  axextndbi  27754  fness  28694  fneref  28696  prtlem13  29153  prtlem15  29160  prtlem17  29161  aomclem8  29554  axc11next  29800  bj-elequ2g  32475  bj-elequ12  32477  bj-axext3  32591  bj-axrep1  32611  bj-axrep2  32612  bj-axrep3  32613  bj-axrep4  32614  bj-nalset  32617  bj-eleq2w  32660  bj-axsep2  32730