Theorem elequ1 1134

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 967	. 2 |- (x = y -> (x e. z -> y e. z))
2		ax-13 967	. . 3 |- (y = x -> (y e. z -> x e. z))
3	2	equcoms 1128	. 2 |- (x = y -> (y e. z -> x e. z))
4	1, 3	impbid 515	1 |- (x = y -> (x e. z <-> y e. z))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954   e. wcel 956

This theorem is referenced by:  cleljust 1326  elsb3 1329  dveel1 1354  ax15 1357  ax11el 1362  axsep 2697  nalset 2707  axpow 2738  dtruALT 2743  axun 2862  pssnn 4519  axinf 4603  aceq0 4710  axac 4725  nd1 4918  axextnd 4923  axrepndlem1 4924  axrepndlem2 4925  axunndlem1 4927  axunnd 4928  axpowndlem2 4930  axpowndlem3 4931  axpowndlem4 4932  axregndlem1 4934  axregndlem2 4935  axregnd 4936  axinfnd 4938  axacndlem5 4943  axacnd 4944  zfcndun 4947  zfcndpow 4948  zfcndinf 4950  zfcndac 4951  tgval3t 7575  tgss2t 7587  basgen2t 7589  axgroth3 8718  axgroth4 8719  grothinf 8720

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-8 962  ax-12 966  ax-13 967  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain