Theorem eleq2d 2420

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eleq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
eleq2d	|- (ph -> (C e. A <-> C e. B))

Proof of Theorem eleq2d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 |- (ph -> A = B)
2		eleq2 2414	. 2 |- (A = B -> (C e. A <-> C e. B))
3	1, 2	syl 15	1 |- (ph -> (C e. A <-> C e. B))

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642   e. wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349

This theorem is referenced by:  eleq12d  2421  eleqtrd  2429  neleqtrd  2448  neleqtrrd  2449  abeq2d  2463  nfceqdf  2489  drnfc1  2506  drnfc2  2507  sbcbid  3100  cbvcsb  3141  sbcel1g  3156  csbeq2d  3161  csbie2g  3183  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202  cbviun  4004  cbviin  4005  iinxsng  4043  iinxprg  4044  iunxsng  4045  nnsucelr  4429  nnadjoin  4521  tfinnn  4535  opeliunxp  4821  opeliunxp2  4823  iunxpf  4830  funfni  5184  fun11iun  5306  fvelrnb  5366  fniniseg  5372  fvun1  5380  eqfnfv  5393  elpreima  5408  dff3  5421  dffo4  5424  eluniima  5470  dff13  5472  isoini  5498  ovelrn  5609  mpteq12f  5656  mpt2eq123dv  5664  cbvmpt2x  5679  ovmpt2x  5713  fmpt2x  5731  clos1basesucg  5885  erref  5960  ereldm  5972  elmapg  6013  elpmg  6014  enpw1  6063  enprmaplem3  6079  nenpw1pwlem2  6086  elce  6176  nmembers1  6272