Theorem eleq2d 2266

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 2260	. 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 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleq12d  2267  eleqtrd  2275  neleqtrd  2294  neleqtrrd  2295  abeq2d  2309  nfceqdf  2338  drnfc1  2356  drnfc2  2357  sbcbid  3047  cbvcsbw  3088  cbvcsb  3089  sbcel1g  3103  csbeq2d  3109  csbie2g  3135  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  opeq1  3809  opeq2  3810  cbviun  3954  cbviin  3955  iinxsng  3991  iinxprg  3992  iunxsng  3993  iunxsngf  3995  cbvdisj  4021  disjnim  4025  disjiun  4029  mpteq12f  4114  axpweq  4205  rabxfrd  4505  onsucelsucexmid  4567  ordsucunielexmid  4568  0elsucexmid  4602  0nelelxp  4693  opeliunxp  4719  opeliunxp2  4807  iunxpf  4815  elrelimasn  5036  elimasng  5038  xpimasn  5119  ressn  5211  funfni  5361  fnbr  5363  fun11iun  5528  fvelrnb  5611  foelcdmi  5616  fvun1  5630  fvco2  5633  elfvmptrab1  5659  elfvmptrab  5660  elpreima  5684  dff3im  5710  resflem  5729  fmptco  5731  funfvima3  5799  foima2  5801  eluniimadm  5815  dff13  5818  f1eqcocnv  5841  isoini  5868  riotaeqdv  5881  mpoeq123dva  5987  cbvmpox  6004  ovelrn  6076  elovmpod  6125  elovmpo  6126  elovmporab  6127  elovmporab1w  6128  fmpox  6262  disjxp1  6298  opeliunxp2f  6300  mpoxopn0yelv  6301  mpoxopovel  6303  rbropapd  6304  rntpos  6319  smoel  6362  smoiso  6364  smoel2  6365  tfrlem9  6381  tfrlemisucaccv  6387  tfrlemiubacc  6392  tfrlemi14d  6395  tfri2d  6398  tfr1onlemubacc  6408  tfr1onlemres  6411  tfrcllemubacc  6421  tfrcllemres  6424  rdgon  6448  freceq1  6454  freceq2  6455  frec0g  6459  frecabcl  6461  freccllem  6464  frecfcllem  6466  frecsuclem  6468  frecsuc  6469  nnsucelsuc  6553  nnsucuniel  6557  nnmordi  6578  ereldm  6641  iinerm  6670  elmapg  6724  elpmg  6727  elixpsn  6798  ixpsnf1o  6799  pw2f1odclem  6899  phplem4  6920  phplem3g  6921  phplem4on  6932  exmidpw  6973  fiintim  6996  fidcenumlemrks  7023  fidcenumlemrk  7024  elfi  7041  ordiso2  7105  ctssdccl  7181  nnnninfeq  7198  cc2lem  7338  cc2  7339  cc3  7340  archnqq  7489  ltdfpr  7578  genpelxp  7583  genpelvl  7584  genpelvu  7585  addcanprleml  7686  addcanprlemu  7687  cauappcvgprlem1  7731  suplocexprlemell  7785  suplocexprlemmu  7790  suplocexprlemru  7791  suplocexprlemdisj  7792  suplocexprlemloc  7793  suplocexprlemub  7795  suplocexprlemlub  7796  cnm  7904  eluz1  9610  elixx1  9977  elioo2  10001  elfz1  10093  elfzp1  10152  fzpr  10157  fzsuc2  10159  fzrev3  10167  elfzp12  10179  fzm1  10180  fzoval  10228  elfzo  10229  fzodcel  10233  elfzom1b  10310  fzosplitsni  10316  nninfdcex  10332  zmodidfzo  10450  frecuzrdgtcl  10509  frecuzrdgfunlem  10516  seqf1og  10618  bcval  10846  bcpasc  10863  wrdmap  10971  elovmpowrd  10981  shftfn  10994  shftval  10995  seq3shft  11008  iser3shft  11516  sumeq1  11525  summodclem3  11550  summodclem2a  11551  isumss  11561  fsumsplit  11577  sumsplitdc  11602  fsum2dlemstep  11604  fisumcom2  11608  fsumparts  11640  explecnv  11675  fprodsplitdc  11766  fprodsplit  11767  fprod2dlemstep  11792  fprodcom2fi  11796  eftlub  11860  divalgmod  12097  bitsval  12113  bitsp1e  12122  bitsp1o  12123  algfx  12233  eucalgcvga  12239  reumodprminv  12435  nnnn0modprm0  12437  ennnfonelemex  12644  ennnfonelemhom  12645  ennnfonelemf1  12648  ennnfonelemrn  12649  ctinfomlemom  12657  ctinfom  12658  ctiunctlemudc  12667  ctiunctlemf  12668  elrest  12936  ptex  12954  prdsbasmpt  12970  prdsbasmpt2  12978  pwselbasb  12983  imasaddfnlemg  13004  divsfval  13018  xpscf  13037  grpidvalg  13063  grpidpropdg  13064  grpidd  13073  issgrpd  13102  sgrppropd  13103  ismndd  13125  mndpropd  13128  ismhm  13140  issubm  13151  imasgrp2  13287  imasgrp  13288  issubg  13350  subginv  13358  isnsg  13379  eqg0el  13406  quselbasg  13407  isghm  13420  resghm2b  13439  conjnmzb  13457  conjnsg  13458  ghmpropd  13460  imasabl  13513  isrngd  13556  rngpropd  13558  imasrng  13559  qusrng  13561  dfur2g  13565  srgidmlem  13581  issrgid  13584  ringcl  13616  isringid  13628  isringd  13644  imasring  13667  oppr0g  13684  oppr1g  13685  reldvdsrsrg  13695  dvdsrvald  13696  isunitd  13709  unitinvcl  13726  unitinvinv  13727  unitlinv  13729  unitrinv  13730  unitnegcl  13733  dvdsrpropdg  13750  isrhm  13761  isrim0  13764  rhmmul  13767  islring  13795  issubrng  13802  opprsubrngg  13814  issubrg  13824  resrhm2b  13852  rhmpropd  13857  rrgval  13865  aprval  13885  aprap  13889  islmod  13894  lmodprop2d  13951  islssm  13960  islssmg  13961  islssmd  13962  lssats2  14017  ellspsn  14020  ixpsnbasval  14069  islidlm  14082  isridlrng  14085  rspssp  14097  rnglidlmmgm  14099  2idlval  14105  isridl  14107  2idlelb  14108  quscrng  14136  rspsn  14137  zrhval  14220  zrhrhmb  14225  znf1o  14254  istopon  14296  eltg  14335  eltg2  14336  eltop  14352  eltop2  14353  eltop3  14354  iscld  14386  neiss2  14425  isnei  14427  lmfval  14475  cnfval  14477  iscn  14480  iscnp  14482  tgcn  14491  tgcnp  14492  lmbrf  14498  cnptopresti  14521  txbas  14541  eltx  14542  txdis  14560  txdis1cn  14561  hmeofvalg  14586  ishmeo  14587  ispsmet  14606  ismet  14627  isxmet  14628  elblps  14673  elbl  14674  elmopn  14729  neibl  14774  metrest  14789  txmetcnp  14801  txmetcn  14802  metcnpd  14803  elcncf  14856  ellimc3apf  14943  limcmpted  14946  cnlimcim  14954  cnlimc  14955  eldvap  14965  dvidsslem  14976  dviaddf  14988  dvimulf  14989  elply  15017  ply1termlem  15025  lgseisenlem3  15360  bj-sels  15607  2omap  15689  nninfall  15703  nninfsellemeq  15708