Theorem elequ1 1173

Description: An identity law for the non-logical predicate.

Assertion

Ref	Expression
elequ1	|- (x = y -> (x e. z <-> y e. z))

Proof of Theorem elequ1

Step	Hyp	Ref	Expression
1		ax-13 1005	. 2 |- (x = y -> (x e. z -> y e. z))
2		ax-13 1005	. . 3 |- (y = x -> (y e. z -> x e. z))
3	2	equcoms 1167	. 2 |- (x = y -> (y e. z -> x e. z))
4	1, 3	impbid 519	1 |- (x = y -> (x e. z <-> y e. z))

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992   e. wcel 994

This theorem is referenced by:  cleljust 1366  elsb3 1370  dveel1 1395  ax15 1398  ax11el 1403  axsep 2776  nalset 2786  zfpow 2819  el 2822  dtru 2831  zfun 3090  pssnn 4681  zfinf 4768  aceq0 4876  zfac 4891  nd1 5092  axextnd 5097  axrepndlem1 5098  axrepndlem2 5099  axunndlem1 5101  axunnd 5102  axpowndlem2 5104  axpowndlem3 5105  axpowndlem4 5106  axregndlem1 5108  axregndlem2 5109  axregnd 5110  axinfnd 5112  axacndlem5 5117  axacnd 5118  zfcndun 5121  zfcndpow 5122  zfcndinf 5124  zfcndac 5125  tgval3 7837  tgss2 7849  basgen2 7851  axgroth3 9051  axgroth4 9052  grothinf 9053  alexsublem4 11499  ist1-2 11603  sstotbnd 11992  ismtyhmeolem 12006  elsb3NEWlem 12222  elequ3 12224

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-8 1000  ax-12 1004  ax-13 1005  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain