Theorem elequ2 2181

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 2179	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax-14 2179	. . 3 |- ( y = x -> ( z e. y -> z e. x ) )
3	2	equcoms 1731	. 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 1472  ax-ie2 1517  ax-8 1527  ax-17 1549  ax-i9 1553  ax-14 2179

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2184  dveel2  2186  axext3  2188  axext4  2189  bm1.1  2190  eleq2w  2267  bm1.3ii  4165  nalset  4174  zfun  4481  fv3  5599  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  acfun  7319  ccfunen  7376  cc1  7377  nninfinf  10588  bdsepnft  15827  bdsepnfALT  15829  bdbm1.3ii  15831  bj-nalset  15835  bj-nnelirr  15893  nninfalllem1  15949  nninfsellemeq  15955  nninfsellemqall  15956  nninfsellemeqinf  15957  nninfomni  15960