Theorem elequ1 1911

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

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 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672

This theorem is referenced by:  cleljust  1912  ax12wdemo  1926  cleljustALT  2102  cleljustALT2  2103  dveel1  2219  axc14  2221  elsb3  2283  axsep  4517  nalset  4533  zfpow  4580  zfun  6603  tz7.48lem  7176  unxpdomlem1  7794  pssnn  7808  zfinf  8162  aceq0  8567  dfac3  8570  dfac5lem2  8573  dfac5lem3  8574  dfac2a  8578  zfac  8908  nd1  9030  axextnd  9034  axrepndlem1  9035  axrepndlem2  9036  axunndlem1  9038  axunnd  9039  axpowndlem2  9041  axpowndlem3  9042  axpowndlem4  9043  axregndlem1  9045  axregnd  9047  zfcndun  9058  zfcndpow  9059  zfcndinf  9061  zfcndac  9062  fpwwe2lem12  9084  axgroth3  9274  axgroth4  9275  nqereu  9372  rpnnen  14356  mdetunilem9  19722  madugsum  19745  neiptopnei  20225  2ndc1stc  20543  nrmr0reg  20841  alexsubALTlem4  21143  xrsmopn  21908  itg2cn  22800  itgcn  22879  sqff1o  24188  dya2iocuni  29178  bnj849  29808  erdsze  29997  untsucf  30409  untangtr  30413  dfon2lem3  30502  dfon2lem6  30505  dfon2lem7  30506  dfon2  30509  axextdist  30517  distel  30521  neibastop2lem  31087  bj-elequ12  31343  bj-axsep  31474  bj-nalset  31475  bj-zfpow  31476  bj-ru0  31607  prtlem5  32494  ax12el  32577  pw2f1ocnv  35963  aomclem8  35990  lcosslsp  40739