Theorem elequ1 1132

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

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   e. wcel 955

This theorem is referenced by:  cleljust 1323  elsb3 1326  dveel1 1349  ax15 1352  ax11el 1357  axsep 2692  nalset 2702  axpow 2733  dtruALT 2738  axun 2858  pssnn 4513  axinf 4595  aceq0 4702  axac 4717  nd1 4910  axextnd 4915  axrepndlem1 4916  axrepndlem2 4917  axunndlem1 4919  axunnd 4920  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axregndlem1 4926  axregndlem2 4927  axregnd 4928  axinfnd 4930  axacndlem5 4935  axacnd 4936  zfcndun 4939  zfcndpow 4940  zfcndinf 4942  zfcndac 4943  tgval3t 7567  tgss2t 7579  basgen2t 7581  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 960  ax-8 961  ax-12 965  ax-13 966  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

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

Copyright terms: Public domain