Theorem elequ1 1138

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

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

This theorem is referenced by:  cleljust 1330  elsb3 1333  dveel1 1358  ax15 1361  ax11el 1366  axsep 2708  nalset 2718  axpow 2750  dtruALT 2755  axun 2874  pssnn 4546  axinf 4639  aceq0 4747  axac 4762  nd1 4957  axextnd 4962  axrepndlem1 4963  axrepndlem2 4964  axunndlem1 4966  axunnd 4967  axpowndlem2 4969  axpowndlem3 4970  axpowndlem4 4971  axregndlem1 4973  axregndlem2 4974  axregnd 4975  axinfnd 4977  axacndlem5 4982  axacnd 4983  zfcndun 4986  zfcndpow 4987  zfcndinf 4989  zfcndac 4990  tgval3t 7631  tgss2t 7643  basgen2t 7645  axgroth3 8781  axgroth4 8782  grothinf 8783

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-8 966  ax-12 970  ax-13 971  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125

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

Copyright terms: Public domain