Theorem elequ1 1136

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

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

This theorem is referenced by:  cleljust 1328  elsb3 1331  dveel1 1356  ax15 1359  ax11el 1364  axsep 2702  nalset 2712  axpow 2743  dtruALT 2748  axun 2867  pssnn 4534  axinf 4623  aceq0 4730  axac 4745  nd1 4938  axextnd 4943  axrepndlem1 4944  axrepndlem2 4945  axunndlem1 4947  axunnd 4948  axpowndlem2 4950  axpowndlem3 4951  axpowndlem4 4952  axregndlem1 4954  axregndlem2 4955  axregnd 4956  axinfnd 4958  axacndlem5 4963  axacnd 4964  zfcndun 4967  zfcndpow 4968  zfcndinf 4970  zfcndac 4971  tgval3t 7625  tgss2t 7637  basgen2t 7639  axgroth3 8779  axgroth4 8780  grothinf 8781

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-8 964  ax-12 968  ax-13 969  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123

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

Copyright terms: Public domain