Theorem elequ1 1894

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

Syntax hints:   -> wi 4   <-> wb 188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664

This theorem is referenced by:  cleljust  1895  ax12wdemo  1909  cleljustALT  2089  cleljustALT2  2090  dveel1  2199  axc14  2201  elsb3  2263  axsep  4524  nalset  4540  zfpow  4582  zfun  6584  tz7.48lem  7158  unxpdomlem1  7776  pssnn  7790  zfinf  8144  aceq0  8549  dfac3  8552  dfac5lem2  8555  dfac5lem3  8556  dfac2a  8560  zfac  8890  nd1  9012  axextnd  9016  axrepndlem1  9017  axrepndlem2  9018  axunndlem1  9020  axunnd  9021  axpowndlem2  9023  axpowndlem3  9024  axpowndlem4  9025  axregndlem1  9027  axregnd  9029  zfcndun  9040  zfcndpow  9041  zfcndinf  9043  zfcndac  9044  fpwwe2lem12  9066  axgroth3  9256  axgroth4  9257  nqereu  9354  rpnnen  14279  mdetunilem9  19645  madugsum  19668  neiptopnei  20148  2ndc1stc  20466  nrmr0reg  20764  alexsubALTlem4  21065  xrsmopn  21830  itg2cn  22721  itgcn  22800  sqff1o  24109  dya2iocuni  29105  bnj849  29736  erdsze  29925  untsucf  30337  untangtr  30341  dfon2lem3  30431  dfon2lem6  30434  dfon2lem7  30435  dfon2  30438  axextdist  30446  distel  30450  neibastop2lem  31016  bj-elequ12  31277  bj-axsep  31408  bj-nalset  31409  bj-zfpow  31410  bj-ru0  31537  prtlem5  32430  ax12el  32513  pw2f1ocnv  35892  aomclem8  35919  lcosslsp  40284