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  4166  nalset  4175  zfun  4482  fv3  5601  tfrlemisucaccv  6413  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  acfun  7321  ccfunen  7378  cc1  7379  nninfinf  10590  bdsepnft  15860  bdsepnfALT  15862  bdbm1.3ii  15864  bj-nalset  15868  bj-nnelirr  15926  nninfalllem1  15982  nninfsellemeq  15988  nninfsellemqall  15989  nninfsellemeqinf  15990  nninfomni  15993