Theorem elequ2 1139

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

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

This theorem is referenced by:  dveel2 1359  dveel2ALT 1364  ax11el 1366  zfext2 1464  bm1.1 1465  axrep1 2699  axrep2 2700  axrep3 2701  axrep4 2702  axsep2 2709  bm1.3ii 2711  nalset 2717  dtruALT 2754  axun 2873  aceq0 4740  axac 4755  nd2 4951  nd3 4952  axrepndlem2 4957  axunndlem1 4959  axunnd 4960  axpowndlem2 4962  axpowndlem3 4963  axpowndlem4 4964  axpownd 4965  axregndlem2 4967  axregnd 4968  axinfndlem1 4969  axacndlem4 4974  axacndlem5 4975  axacnd 4976  zfcndrep 4978  zfcndun 4979  zfcndac 4983  tgss2t 7636  blssopn 7864  axgroth4 8775  uninqs 10436

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