Theorem elequ2 1912

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		ax9 1911	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax9 1911	. . 3 |- ( y = x -> ( z e. y -> z e. x ) )
3	2	equcoms 1875	. 2 |- ( x = y -> ( z e. y -> z e. x ) )
4	1, 3	impbid 195	1 |- ( x = y -> ( z e. x <-> z e. y ) )

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 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675

This theorem is referenced by:  ax12wdemo  1920  dveel2  2211  elsb4  2275  axext3  2444  axext3ALT  2445  axext4  2446  bm1.1  2447  axrep1  4530  axrep2  4531  axrep3  4532  axrep4  4533  bm1.3ii  4542  nalset  4554  fv3  5901  zfun  6611  tz7.48lem  7184  aceq0  8575  dfac2a  8586  axdc3lem2  8907  zfac  8916  nd2  9039  nd3  9040  axrepndlem2  9044  axunndlem1  9046  axunnd  9047  axpowndlem2  9049  axpowndlem3  9050  axpowndlem4  9051  axpownd  9052  axregndlem2  9054  axregnd  9055  axinfndlem1  9056  axacndlem5  9062  zfcndrep  9065  zfcndun  9066  zfcndac  9070  axgroth4  9283  nqereu  9380  rpnnen  14328  mdetunilem9  19694  neiptopnei  20197  2ndc1stc  20515  kqt0lem  20800  regr1lem2  20804  nrmr0reg  20813  hauspwpwf1  21051  dya2iocuni  29154  erdsze  29974  untsucf  30386  untangtr  30390  dfon2lem3  30480  dfon2lem6  30483  dfon2lem7  30484  dfon2lem8  30485  dfon2  30487  axext4dist  30496  distel  30499  axextndbi  30500  fness  31054  fneref  31055  bj-elequ2g  31320  bj-elequ12  31322  bj-axext3  31429  bj-axrep1  31448  bj-axrep2  31449  bj-axrep3  31450  bj-axrep4  31451  bj-nalset  31454  bj-eleq2w  31501  bj-axsep2  31573  prtlem13  32485  prtlem15  32492  prtlem17  32493  dveel2ALT  32555  ax12el  32558  aomclem8  35964  elintima  36290  axc11next  36801