Theorem elequ1 1770

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

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 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769

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

This theorem is referenced by:  ax12wdemo  1780  cleljust  2082  cleljustALT  2083  dveel1  2084  axc14  2086  elsb3  2161  ax12el  2265  axsep  4567  nalset  4584  zfpow  4626  zfun  6577  tz7.48lem  7106  unxpdomlem1  7724  pssnn  7738  zfinf  8056  aceq0  8499  dfac3  8502  dfac5lem2  8505  dfac5lem3  8506  dfac2a  8510  zfac  8840  nd1  8962  axextnd  8966  axrepndlem1  8967  axrepndlem2  8968  axunndlem1  8970  axunnd  8971  axpowndlem2  8973  axpowndlem2OLD  8974  axpowndlem3  8975  axpowndlem3OLD  8976  axpowndlem4  8977  axregndlem1  8979  axregnd  8981  axregndOLD  8982  zfcndun  8993  zfcndpow  8994  zfcndinf  8996  zfcndac  8997  fpwwe2lem12  9019  axgroth3  9209  axgroth4  9210  nqereu  9307  rpnnen  13821  madugsum  18940  neiptopnei  19427  2ndc1stc  19746  nrmr0reg  20013  alexsubALTlem4  20313  xrsmopn  21080  itg2cn  21933  itgcn  22012  sqff1o  23212  dya2iocuni  27922  erdsze  28314  untsucf  28585  untangtr  28589  dfon2lem3  28822  dfon2lem6  28825  dfon2lem7  28826  dfon2  28829  axextdist  28837  distel  28841  neibastop2lem  29809  prtlem5  30229  pw2f1ocnv  30611  aomclem8  30639  lcosslsp  32138  bnj849  33080  bj-elequ12  33339  bj-cleljust  33443  bj-axsep  33478  bj-nalset  33479  bj-zfpow  33480  bj-ru0  33599