Theorem elequ1 1822

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 1821	. 2 |- ( x = y -> ( x e. z -> y e. z ) )
2		ax-8 1821	. . 3 |- ( y = x -> ( y e. z -> x e. z ) )
3	2	equcoms 1796	. 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 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821

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

This theorem is referenced by:  ax12wdemo  1832  cleljust  2110  cleljustALT  2111  dveel1  2112  axc14  2114  elsb3  2179  ax12el  2273  axsep  4577  nalset  4593  zfpow  4635  zfun  6592  tz7.48lem  7124  unxpdomlem1  7743  pssnn  7757  zfinf  8073  aceq0  8516  dfac3  8519  dfac5lem2  8522  dfac5lem3  8523  dfac2a  8527  zfac  8857  nd1  8979  axextnd  8983  axrepndlem1  8984  axrepndlem2  8985  axunndlem1  8987  axunnd  8988  axpowndlem2  8990  axpowndlem2OLD  8991  axpowndlem3  8992  axpowndlem3OLD  8993  axpowndlem4  8994  axregndlem1  8996  axregnd  8998  axregndOLD  8999  zfcndun  9010  zfcndpow  9011  zfcndinf  9013  zfcndac  9014  fpwwe2lem12  9036  axgroth3  9226  axgroth4  9227  nqereu  9324  rpnnen  13972  mdetunilem9  19249  madugsum  19272  neiptopnei  19760  2ndc1stc  20078  nrmr0reg  20376  alexsubALTlem4  20676  xrsmopn  21443  itg2cn  22296  itgcn  22375  sqff1o  23582  dya2iocuni  28427  erdsze  28843  untsucf  29300  untangtr  29304  dfon2lem3  29434  dfon2lem6  29437  dfon2lem7  29438  dfon2  29441  axextdist  29449  distel  29453  neibastop2lem  30383  prtlem5  30802  pw2f1ocnv  31183  aomclem8  31211  lcosslsp  33183  bnj849  34126  bj-elequ12  34382  bj-cleljust  34487  bj-axsep  34522  bj-nalset  34523  bj-zfpow  34524  bj-ru0  34643