Theorem elequ1 1873

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

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

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 1751  ax-6 1797  ax-7 1841  ax-8 1872

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

This theorem is referenced by:  ax12wdemo  1883  cleljust  2163  cleljustALT  2164  dveel1  2165  axc14  2167  elsb3  2230  axsep  4547  nalset  4562  zfpow  4604  zfun  6598  tz7.48lem  7166  unxpdomlem1  7782  pssnn  7796  zfinf  8144  aceq0  8547  dfac3  8550  dfac5lem2  8553  dfac5lem3  8554  dfac2a  8558  zfac  8888  nd1  9010  axextnd  9014  axrepndlem1  9015  axrepndlem2  9016  axunndlem1  9018  axunnd  9019  axpowndlem2  9021  axpowndlem3  9022  axpowndlem4  9023  axregndlem1  9025  axregnd  9027  axregndOLD  9028  zfcndun  9039  zfcndpow  9040  zfcndinf  9042  zfcndac  9043  fpwwe2lem12  9065  axgroth3  9255  axgroth4  9256  nqereu  9353  rpnnen  14257  mdetunilem9  19576  madugsum  19599  neiptopnei  20079  2ndc1stc  20397  nrmr0reg  20695  alexsubALTlem4  20996  xrsmopn  21741  itg2cn  22598  itgcn  22677  sqff1o  23972  dya2iocuni  28944  bnj849  29524  erdsze  29713  untsucf  30125  untangtr  30129  dfon2lem3  30218  dfon2lem6  30221  dfon2lem7  30222  dfon2  30225  axextdist  30233  distel  30237  neibastop2lem  30801  bj-elequ12  31019  bj-cleljust  31124  bj-axsep  31159  bj-nalset  31160  bj-zfpow  31161  bj-ru0  31286  prtlem5  32139  ax12el  32225  pw2f1ocnv  35601  aomclem8  35628  lcosslsp  39003