Theorem elequ2 2169

Description: An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem elequ2

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

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541  ax-14 2167

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2172  dveel2  2174  axext3  2176  axext4  2177  bm1.1  2178  eleq2w  2255  bm1.3ii  4150  nalset  4159  zfun  4465  fv3  5577  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  acfun  7267  ccfunen  7324  cc1  7325  nninfinf  10514  bdsepnft  15379  bdsepnfALT  15381  bdbm1.3ii  15383  bj-nalset  15387  bj-nnelirr  15445  nninfalllem1  15498  nninfsellemeq  15504  nninfsellemqall  15505  nninfsellemeqinf  15506  nninfomni  15509