Theorem elequ2 2172

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 2170	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax-14 2170	. . 3 |- ( y = x -> ( z e. y -> z e. x ) )
3	2	equcoms 1722	. 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 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544  ax-14 2170

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2175  dveel2  2177  axext3  2179  axext4  2180  bm1.1  2181  eleq2w  2258  bm1.3ii  4154  nalset  4163  zfun  4469  fv3  5581  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  acfun  7274  ccfunen  7331  cc1  7332  nninfinf  10535  bdsepnft  15533  bdsepnfALT  15535  bdbm1.3ii  15537  bj-nalset  15541  bj-nnelirr  15599  nninfalllem1  15652  nninfsellemeq  15658  nninfsellemqall  15659  nninfsellemeqinf  15660  nninfomni  15663