Theorem elequ2 1137

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

Assertion

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

Proof of Theorem elequ2

Step	Hyp	Ref	Expression
1		ax-14 970	. 2 |- (x = y -> (z e. x -> z e. y))
2		ax-14 970	. . 3 |- (y = x -> (z e. y -> z e. x))
3	2	equcoms 1130	. 2 |- (x = y -> (z e. y -> z e. x))
4	1, 3	impbid 516	1 |- (x = y -> (z e. x <-> z e. y))

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

This theorem is referenced by:  dveel2 1357  dveel2ALT 1362  ax11el 1364  zfext2 1461  bm1.1 1462  axrep1 2694  axrep2 2695  axrep3 2696  axrep4 2697  axsep2 2704  bm1.3ii 2706  nalset 2712  dtruALT 2748  axun 2867  aceq0 4722  axac 4737  nd2 4931  nd3 4932  axrepndlem2 4937  axunndlem1 4939  axunnd 4940  axpowndlem2 4942  axpowndlem3 4943  axpowndlem4 4944  axpownd 4945  axregndlem2 4947  axregnd 4948  axinfndlem1 4949  axacndlem4 4954  axacndlem5 4955  axacnd 4956  zfcndrep 4958  zfcndun 4959  zfcndac 4963  tgss2t 7622  blssopn 7852  axgroth4 8765  uninqs 10425

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-14 970  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