Theorem elequ2 2207

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 2205	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax-14 2205	. . 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 1497  ax-ie2 1542  ax-8 1552  ax-17 1574  ax-i9 1578  ax-14 2205

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2210  dveel2  2212  axext3  2214  axext4  2215  bm1.1  2216  eleq2w  2293  bm1.3ii  4210  nalset  4219  zfun  4531  fv3  5662  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  sspw1or2  7403  acfun  7422  ccfunen  7483  cc1  7484  nninfinf  10706  bdsepnft  16533  bdsepnfALT  16535  bdbm1.3ii  16537  bj-nalset  16541  bj-nnelirr  16599  nninfalllem1  16661  nninfsellemeq  16667  nninfsellemqall  16668  nninfsellemeqinf  16669  nninfomni  16672