Theorem eleq2d 2301

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 2295	. 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 1398   e. wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12d  2302  eleqtrd  2310  neleqtrd  2329  neleqtrrd  2330  abeq2d  2344  nfceqdf  2374  drnfc1  2392  drnfc2  2393  sbcbid  3090  cbvcsbw  3132  cbvcsb  3133  sbcel1g  3147  csbeq2d  3153  csbie2g  3179  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  rabsnif  3742  opeq1  3867  opeq2  3868  cbviun  4012  cbviin  4013  iinxsng  4049  iinxprg  4050  iunxsng  4051  iunxsngf  4053  cbvdisj  4079  disjnim  4083  disjiun  4088  mpteq12f  4174  axpweq  4267  rabxfrd  4572  onsucelsucexmid  4634  ordsucunielexmid  4635  0elsucexmid  4669  0nelelxp  4760  opeliunxp  4787  opeliunxp2  4876  iunxpf  4884  elrelimasn  5109  elimasng  5111  xpimasn  5192  ressn  5284  funfni  5439  fnbr  5441  fun11iun  5613  fvelrnb  5702  foelcdmi  5707  fvun1  5721  fvco2  5724  elfvmptrab1  5750  elfvmptrab  5751  elpreima  5775  dff3im  5800  resflem  5819  fmptco  5821  funfvima3  5898  foima2  5902  eluniimadm  5916  dff13  5919  f1eqcocnv  5942  isoini  5969  riotaeqdv  5982  mpoeq123dva  6092  cbvmpox  6109  ovelrn  6181  elovmpod  6230  elovmpo  6231  elovmporab  6232  elovmporab1w  6233  fmpox  6374  disjxp1  6410  elsuppfng  6420  elsuppfn  6421  suppfnss  6435  suppcofn  6444  opeliunxp2f  6447  mpoxopn0yelv  6448  mpoxopovel  6450  rbropapd  6451  rntpos  6466  smoel  6509  smoiso  6511  smoel2  6512  tfrlem9  6528  tfrlemisucaccv  6534  tfrlemiubacc  6539  tfrlemi14d  6542  tfri2d  6545  tfr1onlemubacc  6555  tfr1onlemres  6558  tfrcllemubacc  6568  tfrcllemres  6571  rdgon  6595  freceq1  6601  freceq2  6602  frec0g  6606  frecabcl  6608  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnsucelsuc  6702  nnsucuniel  6706  nnmordi  6727  ereldm  6790  iinerm  6819  elmapg  6873  elpmg  6876  elixpsn  6947  ixpsnf1o  6948  pw2f1odclem  7063  phplem4  7084  phplem3g  7085  phplem4on  7097  exmidpw  7143  fiintim  7166  fidcenumlemrks  7195  fidcenumlemrk  7196  elfi  7213  ordiso2  7277  ctssdccl  7353  nnnninfeq  7370  cc2lem  7528  cc2  7529  cc3  7530  archnqq  7680  ltdfpr  7769  genpelxp  7774  genpelvl  7775  genpelvu  7776  addcanprleml  7877  addcanprlemu  7878  cauappcvgprlem1  7922  suplocexprlemell  7976  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  cnm  8095  eluz1  9802  elixx1  10175  elioo2  10199  elfz1  10291  elfzp1  10350  fzpr  10355  fzsuc2  10357  fzrev3  10365  elfzp12  10377  fzm1  10378  fzoval  10426  elfzo  10427  fzodcel  10431  elfzom1b  10518  fzosplitsni  10525  nninfdcex  10541  zmodidfzo  10659  frecuzrdgtcl  10718  frecuzrdgfunlem  10725  seqf1og  10827  bcval  11055  bcpasc  11072  fundm2domnop0  11156  wrdmap  11192  elovmpowrd  11202  ccatfvalfi  11216  elfzelfzccat  11224  ccatlid  11230  ccatass  11232  ccatrn  11233  ccatalpha  11237  swrdfv2  11291  ccatswrd  11298  swrdccat2  11299  pfxfv  11312  pfxeq  11324  ccatpfx  11329  swrdswrd  11333  swrdpfx  11335  pfxpfx  11336  cats1un  11349  swrdccatfn  11352  swrdccatin1  11353  pfxccatin12lem4  11354  pfxccatin12lem1  11356  swrdccatin2  11357  pfxccatin12lem2c  11358  pfxccatin12lem2  11359  swrdccat3blem  11367  swrdccatin1d  11371  swrdccatin2d  11372  pfxccatin12d  11373  shftfn  11445  shftval  11446  seq3shft  11459  iser3shft  11967  sumeq1  11976  summodclem3  12002  summodclem2a  12003  isumss  12013  fsumsplit  12029  sumsplitdc  12054  fsum2dlemstep  12056  fisumcom2  12060  fsumparts  12092  explecnv  12127  fprodsplitdc  12218  fprodsplit  12219  fprod2dlemstep  12244  fprodcom2fi  12248  eftlub  12312  divalgmod  12549  bitsval  12565  bitsp1e  12574  bitsp1o  12575  algfx  12685  eucalgcvga  12691  reumodprminv  12887  nnnn0modprm0  12889  ennnfonelemex  13096  ennnfonelemhom  13097  ennnfonelemf1  13100  ennnfonelemrn  13101  ctinfomlemom  13109  ctinfom  13110  ctiunctlemudc  13119  ctiunctlemf  13120  elrest  13390  ptex  13408  prdsbasmpt  13424  prdsbasmpt2  13432  pwselbasb  13437  imasaddfnlemg  13458  divsfval  13472  xpscf  13491  grpidvalg  13517  grpidpropdg  13518  grpidd  13527  issgrpd  13556  sgrppropd  13557  ismndd  13581  mndpropd  13584  imasmnd2  13596  imasmnd  13597  ismhm  13605  issubm  13616  imasgrp2  13758  imasgrp  13759  issubg  13821  subginv  13829  isnsg  13850  eqg0el  13877  quselbasg  13878  isghm  13891  resghm2b  13910  conjnmzb  13928  conjnsg  13929  ghmpropd  13931  imasabl  13984  gsumsplit0  13994  isrngd  14028  rngpropd  14030  imasrng  14031  qusrng  14033  dfur2g  14037  srgidmlem  14053  issrgid  14056  ringcl  14088  isringid  14100  isringd  14116  imasring  14139  oppr0g  14156  oppr1g  14157  dvdsrvald  14169  isunitd  14182  unitinvcl  14199  unitinvinv  14200  unitlinv  14202  unitrinv  14203  unitnegcl  14206  dvdsrpropdg  14223  isrhm  14234  isrim0  14237  rhmmul  14240  islring  14268  issubrng  14275  opprsubrngg  14287  issubrg  14297  resrhm2b  14325  rhmpropd  14330  rrgval  14338  aprval  14358  aprap  14362  islmod  14367  lmodprop2d  14424  islssm  14433  islssmg  14434  islssmd  14435  lssats2  14490  ellspsn  14493  ixpsnbasval  14542  islidlm  14555  isridlrng  14558  rspssp  14570  rnglidlmmgm  14572  2idlval  14578  isridl  14580  2idlelb  14581  quscrng  14609  rspsn  14610  zrhval  14693  zrhrhmb  14698  znf1o  14727  psrgrp  14766  mplelbascoe  14773  istopon  14804  eltg  14843  eltg2  14844  eltop  14860  eltop2  14861  eltop3  14862  iscld  14894  neiss2  14933  isnei  14935  lmfval  14984  cnfval  14985  iscn  14988  iscnp  14990  tgcn  14999  tgcnp  15000  lmbrf  15006  cnptopresti  15029  txbas  15049  eltx  15050  txdis  15068  txdis1cn  15069  hmeofvalg  15094  ishmeo  15095  ispsmet  15114  ismet  15135  isxmet  15136  elblps  15181  elbl  15182  elmopn  15237  neibl  15282  metrest  15297  txmetcnp  15309  txmetcn  15310  metcnpd  15311  elcncf  15364  ellimc3apf  15451  limcmpted  15454  cnlimcim  15462  cnlimc  15463  eldvap  15473  dvidsslem  15484  dviaddf  15496  dvimulf  15497  elply  15525  ply1termlem  15533  lgseisenlem3  15871  edgval  15981  edgiedgbg  15986  edgupgren  16062  upgredg  16065  uhgr2edg  16127  umgr2edg1  16130  usgredg2vlem1  16143  usgredg2vlem2  16144  ushgredgedg  16147  ushgredgedgloop  16149  subgruhgredgdm  16191  uhgrspansubgrlem  16197  vtxdgfval  16209  vtxedgfi  16210  vtxdgop  16213  vtxdg0v  16215  vtxdeqd  16217  vtxdfifiun  16218  1loopgrvd0fi  16227  1hevtxdg0fi  16228  1hevtxdg1en  16229  wksfval  16243  iswlk  16244  wlkm  16260  uspgr2wlkeq  16286  wlkreslem  16299  wlkres  16300  istrl  16306  clwwlkg  16314  isclwwlk  16315  clwwlkccatlem  16321  isclwwlkng  16327  clwwlkn0  16329  clwwlknnn  16333  clwwlkext2edg  16343  clwwlknonmpo  16349  clwwlknon  16350  clwwlk0on0  16352  iseupth  16368  eupth2lem3lem3fi  16391  eupth2lem3lem6fi  16392  eupth2lem3lem4fi  16394  eupth2lembfi  16398  bj-sels  16610  2omap  16695  pw1map  16697  nninfall  16715  nninfsellemeq  16720