Theorem elequ2 1691

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie2 1470  ax-8 1482  ax-14 1492  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  elsb4  1952  dveel2  1996  axext3  2122  axext4  2123  bm1.1  2124  eleq2w  2201  bm1.3ii  4049  nalset  4058  zfun  4356  fv3  5444  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  acfun  7063  ccfunen  7079  bdsepnft  13085  bdsepnfALT  13087  bdbm1.3ii  13089  bj-nalset  13093  bj-nnelirr  13151  strcollnft  13182  strcollnfALT  13184  nninfalllem1  13203  nninfsellemeq  13210  nninfsellemqall  13211  nninfsellemeqinf  13212  nninfomni  13215