Theorem elequ2 2205

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 2203	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax-14 2203	. . 3 |- ( y = x -> ( z e. y -> z e. x ) )
3	2	equcoms 1754	. 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 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576  ax-14 2203

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2208  dveel2  2210  axext3  2212  axext4  2213  bm1.1  2214  eleq2w  2291  bm1.3ii  4205  nalset  4214  zfun  4525  fv3  5650  tfrlemisucaccv  6471  tfr1onlemsucaccv  6487  tfrcllemsucaccv  6500  acfun  7389  ccfunen  7450  cc1  7451  nninfinf  10665  bdsepnft  16250  bdsepnfALT  16252  bdbm1.3ii  16254  bj-nalset  16258  bj-nnelirr  16316  nninfalllem1  16374  nninfsellemeq  16380  nninfsellemqall  16381  nninfsellemeqinf  16382  nninfomni  16385