Theorem elequ2 2208

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 2206	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax-14 2206	. . 3 |- ( y = x -> ( z e. y -> z e. x ) )
3	2	equcoms 1756	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579  ax-14 2206

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2211  dveel2  2213  axext3  2215  axext4  2216  bm1.1  2217  eleq2w  2294  bm1.3ii  4231  nalset  4240  zfun  4555  fv3  5693  tfrlemisucaccv  6556  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  sspw1or2  7495  acfun  7514  ccfunen  7578  cc1  7579  nninfinf  10805  bdsepnft  16657  bdsepnfALT  16659  bdbm1.3ii  16661  bj-nalset  16665  bj-nnelirr  16723  nninfalllem1  16786  nninfsellemeq  16792  nninfsellemqall  16793  nninfsellemeqinf  16794  nninfomni  16797