Theorem elequ2 2207

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 2205	. 2 |- ( x = y -> ( z e. x -> z e. y ) )
2		ax-14 2205	. . 3 |- ( y = x -> ( z e. y -> z e. x ) )
3	2	equcoms 1756	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579  ax-14 2205

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2210  dveel2  2212  axext3  2214  axext4  2215  bm1.1  2216  eleq2w  2293  bm1.3ii  4215  nalset  4224  zfun  4537  fv3  5671  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  sspw1or2  7463  acfun  7482  ccfunen  7543  cc1  7544  nninfinf  10768  bdsepnft  16603  bdsepnfALT  16605  bdbm1.3ii  16607  bj-nalset  16611  bj-nnelirr  16669  nninfalllem1  16734  nninfsellemeq  16740  nninfsellemqall  16741  nninfsellemeqinf  16742  nninfomni  16745