Theorem elequ2 1135

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

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

This theorem is referenced by:  dveel2 1355  dveel2ALT 1360  ax11el 1362  zfext2 1459  bm1.1 1460  axrep1 2689  axrep2 2690  axrep3 2691  axrep4 2692  axsep2 2699  bm1.3ii 2701  nalset 2707  dtruALT 2743  axun 2862  aceq0 4710  axac 4725  nd2 4919  nd3 4920  axrepndlem2 4925  axunndlem1 4927  axunnd 4928  axpowndlem2 4930  axpowndlem3 4931  axpowndlem4 4932  axpownd 4933  axregndlem2 4935  axregnd 4936  axinfndlem1 4937  axacndlem4 4942  axacndlem5 4943  axacnd 4944  zfcndrep 4946  zfcndun 4947  zfcndac 4951  tgss2t 7587  blssopn 7819  axgroth4 8719  uninqs 10378

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