Theorem elequ1 1759

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 1758	. 2 |- ( x = y -> ( x e. z -> y e. z ) )
2		ax-8 1758	. . 3 |- ( y = x -> ( y e. z -> x e. z ) )
3	2	equcoms 1733	. 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 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758

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

This theorem is referenced by:  ax12wdemo  1769  cleljust  2059  cleljustALT  2060  dveel1  2061  axc14  2063  elsb3  2139  ax12el  2243  axsep  4417  nalset  4434  zfpow  4476  zfun  6378  tz7.48lem  6901  unxpdomlem1  7522  pssnn  7536  zfinf  7850  aceq0  8293  dfac3  8296  dfac5lem2  8299  dfac5lem3  8300  dfac2a  8304  zfac  8634  nd1  8756  axextnd  8760  axrepndlem1  8761  axrepndlem2  8762  axunndlem1  8764  axunnd  8765  axpowndlem2  8767  axpowndlem2OLD  8768  axpowndlem3  8769  axpowndlem3OLD  8770  axpowndlem4  8771  axregndlem1  8773  axregnd  8775  axregndOLD  8776  zfcndun  8787  zfcndpow  8788  zfcndinf  8790  zfcndac  8791  fpwwe2lem12  8813  axgroth3  9003  axgroth4  9004  nqereu  9103  rpnnen  13514  madugsum  18454  neiptopnei  18741  2ndc1stc  19060  nrmr0reg  19327  alexsubALTlem4  19627  xrsmopn  20394  itg2cn  21246  itgcn  21325  sqff1o  22525  dya2iocuni  26703  erdsze  27095  untsucf  27366  untangtr  27370  dfon2lem3  27603  dfon2lem6  27606  dfon2lem7  27607  dfon2  27610  axextdist  27618  distel  27622  neibastop2lem  28586  prtlem5  29006  pw2f1ocnv  29391  aomclem8  29419  lcosslsp  30977  bnj849  31923  bj-elequ12  32180  bj-cleljust  32284  bj-axsep  32319  bj-nalset  32320  bj-zfpow  32321  bj-ru0  32440