Theorem elequ2 2133

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 2131	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax-14 2131	. . 3 |- ( y = x -> ( z e. y -> z e. x ) )
3	2	equcoms 1688	. 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 1429  ax-ie2 1474  ax-8 1484  ax-17 1506  ax-i9 1510  ax-14 2131

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  elsb4  2136  dveel2  2138  axext3  2140  axext4  2141  bm1.1  2142  eleq2w  2219  bm1.3ii  4085  nalset  4094  zfun  4394  fv3  5490  tfrlemisucaccv  6269  tfr1onlemsucaccv  6285  tfrcllemsucaccv  6298  acfun  7136  ccfunen  7178  cc1  7179  bdsepnft  13433  bdsepnfALT  13435  bdbm1.3ii  13437  bj-nalset  13441  bj-nnelirr  13499  nninfalllem1  13551  nninfsellemeq  13557  nninfsellemqall  13558  nninfsellemeqinf  13559  nninfomni  13562