Theorem eleq2d 2247

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 2241	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   e. wcel 2148

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-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12d  2248  eleqtrd  2256  neleqtrd  2275  neleqtrrd  2276  abeq2d  2290  nfceqdf  2318  drnfc1  2336  drnfc2  2337  sbcbid  3021  cbvcsbw  3062  cbvcsb  3063  sbcel1g  3077  csbeq2d  3083  csbie2g  3108  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  opeq1  3779  opeq2  3780  cbviun  3924  cbviin  3925  iinxsng  3961  iinxprg  3962  iunxsng  3963  iunxsngf  3965  cbvdisj  3991  disjnim  3995  disjiun  3999  mpteq12f  4084  axpweq  4172  rabxfrd  4470  onsucelsucexmid  4530  ordsucunielexmid  4531  0elsucexmid  4565  0nelelxp  4656  opeliunxp  4682  opeliunxp2  4768  iunxpf  4776  elrelimasn  4995  elimasng  4997  xpimasn  5078  ressn  5170  funfni  5317  fnbr  5319  fun11iun  5483  fvelrnb  5564  foelcdmi  5569  fvun1  5583  fvco2  5586  elfvmptrab1  5611  elfvmptrab  5612  elpreima  5636  dff3im  5662  resflem  5681  fmptco  5683  funfvima3  5751  foima2  5753  eluniimadm  5766  dff13  5769  f1eqcocnv  5792  isoini  5819  riotaeqdv  5832  mpoeq123dva  5936  cbvmpox  5953  ovelrn  6023  elovmpo  6072  fmpox  6201  disjxp1  6237  opeliunxp2f  6239  mpoxopn0yelv  6240  mpoxopovel  6242  rbropapd  6243  rntpos  6258  smoel  6301  smoiso  6303  smoel2  6304  tfrlem9  6320  tfrlemisucaccv  6326  tfrlemiubacc  6331  tfrlemi14d  6334  tfri2d  6337  tfr1onlemubacc  6347  tfr1onlemres  6350  tfrcllemubacc  6360  tfrcllemres  6363  rdgon  6387  freceq1  6393  freceq2  6394  frec0g  6398  frecabcl  6400  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  nnsucelsuc  6492  nnsucuniel  6496  nnmordi  6517  ereldm  6578  iinerm  6607  elmapg  6661  elpmg  6664  elixpsn  6735  ixpsnf1o  6736  phplem4  6855  phplem3g  6856  phplem4on  6867  exmidpw  6908  fiintim  6928  fidcenumlemrks  6952  fidcenumlemrk  6953  elfi  6970  ordiso2  7034  ctssdccl  7110  nnnninfeq  7126  cc2lem  7265  cc2  7266  cc3  7267  archnqq  7416  ltdfpr  7505  genpelxp  7510  genpelvl  7511  genpelvu  7512  addcanprleml  7613  addcanprlemu  7614  cauappcvgprlem1  7658  suplocexprlemell  7712  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  suplocexprlemlub  7723  cnm  7831  eluz1  9532  elixx1  9897  elioo2  9921  elfz1  10013  elfzp1  10072  fzpr  10077  fzsuc2  10079  fzrev3  10087  elfzp12  10099  fzm1  10100  fzoval  10148  elfzo  10149  fzodcel  10152  elfzom1b  10229  fzosplitsni  10235  zmodidfzo  10353  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  bcval  10729  bcpasc  10746  shftfn  10833  shftval  10834  seq3shft  10847  iser3shft  11354  sumeq1  11363  summodclem3  11388  summodclem2a  11389  isumss  11399  fsumsplit  11415  sumsplitdc  11440  fsum2dlemstep  11442  fisumcom2  11446  fsumparts  11478  explecnv  11513  fprodsplitdc  11604  fprodsplit  11605  fprod2dlemstep  11630  fprodcom2fi  11634  eftlub  11698  divalgmod  11932  nninfdcex  11954  algfx  12052  eucalgcvga  12058  reumodprminv  12253  nnnn0modprm0  12255  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemf1  12419  ennnfonelemrn  12420  ctinfomlemom  12428  ctinfom  12429  ctiunctlemudc  12438  ctiunctlemf  12439  elrest  12695  ptex  12713  imasaddfnlemg  12735  xpscf  12766  grpidvalg  12792  grpidpropdg  12793  grpidd  12802  ismndd  12838  mndpropd  12841  ismhm  12853  issubm  12863  issubg  13033  subginv  13041  isnsg  13062  dfur2g  13145  srgidmlem  13161  issrgid  13164  ringcl  13196  isringid  13208  isringd  13220  oppr0g  13251  oppr1g  13252  reldvdsrsrg  13261  dvdsrvald  13262  isunitd  13275  unitinvcl  13292  unitinvinv  13293  unitlinv  13295  unitrinv  13296  unitnegcl  13299  dvdsrpropdg  13316  islring  13333  issubrg  13342  aprval  13372  aprap  13376  islmod  13381  lmodprop2d  13438  istopon  13516  eltg  13555  eltg2  13556  eltop  13572  eltop2  13573  eltop3  13574  iscld  13606  neiss2  13645  isnei  13647  lmfval  13695  cnfval  13697  iscn  13700  iscnp  13702  tgcn  13711  tgcnp  13712  lmbrf  13718  cnptopresti  13741  txbas  13761  eltx  13762  txdis  13780  txdis1cn  13781  hmeofvalg  13806  ishmeo  13807  ispsmet  13826  ismet  13847  isxmet  13848  elblps  13893  elbl  13894  elmopn  13949  neibl  13994  metrest  14009  txmetcnp  14021  txmetcn  14022  metcnpd  14023  elcncf  14063  ellimc3apf  14132  limcmpted  14135  cnlimcim  14143  cnlimc  14144  eldvap  14154  dviaddf  14172  dvimulf  14173  bj-sels  14669  nninfall  14761  nninfsellemeq  14766