Theorem eleq2d 2304

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 2298	. 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 2205

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 2216

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

This theorem is referenced by:  eleq12d  2305  eleqtrd  2313  neleqtrd  2332  neleqtrrd  2333  abeq2d  2347  eqabrd  2372  nfceqdf  2385  drnfc1  2403  drnfc2  2404  sbcbid  3102  cbvcsbw  3144  cbvcsb  3145  sbcel1g  3159  csbeq2d  3165  csbie2g  3191  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  cbvrabcsf  3206  rabsnif  3760  opeq1  3885  opeq2  3886  cbviun  4030  cbviin  4031  iinxsng  4067  iinxprg  4068  iunxsng  4069  iunxsngf  4071  cbvdisj  4097  disjnim  4101  disjiun  4106  mpteq12f  4192  axpweq  4286  rabxfrd  4592  onsucelsucexmid  4654  ordsucunielexmid  4655  0elsucexmid  4689  0nelelxp  4780  opeliunxp  4807  opeliunxp2  4897  iunxpf  4905  elrelimasn  5130  elimasng  5132  xpimasn  5213  ressn  5305  funfni  5460  fnbr  5462  fun11iun  5637  fvelrnb  5726  foelcdmi  5731  fvun1  5745  fvco2  5748  elfvmptrab1  5774  elfvmptrab  5775  elpreima  5799  dff3im  5824  resflem  5843  fmptco  5845  funfvima3  5922  foima2  5926  eluniimadm  5940  dff13  5943  f1eqcocnv  5966  isoini  5993  riotaeqdv  6006  mpoeq123dva  6116  cbvmpox  6133  ovelrn  6205  elovmpod  6254  elovmpo  6255  elovmporab  6256  elovmporab1w  6257  fmpox  6398  disjxp1  6434  elsuppfng  6444  elsuppfn  6445  suppfnss  6459  suppcofn  6468  opeliunxp2f  6471  mpoxopn0yelv  6472  mpoxopovel  6474  rbropapd  6475  rntpos  6490  smoel  6533  smoiso  6535  smoel2  6536  tfrlem9  6552  tfrlemisucaccv  6558  tfrlemiubacc  6563  tfrlemi14d  6566  tfri2d  6569  tfr1onlemubacc  6579  tfr1onlemres  6582  tfrcllemubacc  6592  tfrcllemres  6595  rdgon  6619  freceq1  6625  freceq2  6626  frec0g  6630  frecabcl  6632  freccllem  6635  frecfcllem  6637  frecsuclem  6639  frecsuc  6640  nnsucelsuc  6726  nnsucuniel  6730  nnmordi  6751  ereldm  6814  iinerm  6843  elmapg  6897  elpmg  6900  elixpsn  6972  ixpsnf1o  6973  pw2f1odclem  7089  phplem4  7111  phplem3g  7112  phplem4on  7124  exmidpw  7170  fiintim  7193  fidcenumlemrks  7225  fidcenumlemrk  7226  elfi  7260  2omap  7271  ordiso2  7328  ctssdccl  7404  nnnninfeq  7421  cc2lem  7582  cc2  7583  cc3  7584  archnqq  7734  ltdfpr  7823  genpelxp  7828  genpelvl  7829  genpelvu  7830  addcanprleml  7931  addcanprlemu  7932  cauappcvgprlem1  7976  suplocexprlemell  8030  suplocexprlemmu  8035  suplocexprlemru  8036  suplocexprlemdisj  8037  suplocexprlemloc  8038  suplocexprlemub  8040  suplocexprlemlub  8041  cnm  8149  eluz1  9860  elixx1  10233  elioo2  10257  elfz1  10350  elfzp1  10410  fzpr  10415  fzsuc2  10417  fzrev3  10425  elfzp12  10437  fzm1  10438  fzoval  10486  elfzo  10487  fzodcel  10491  elfzom1b  10578  fzosplitsni  10585  nninfdcex  10601  zmodidfzo  10719  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  seqf1og  10887  bcval  11115  bcpasc  11132  fundm2domnop0  11224  wrdmap  11260  elovmpowrd  11270  ccatfvalfi  11284  elfzelfzccat  11292  ccatlid  11298  ccatass  11300  ccatrn  11301  ccatalpha  11305  swrdfv2  11359  ccatswrd  11366  swrdccat2  11367  pfxfv  11380  pfxeq  11392  ccatpfx  11397  swrdswrd  11401  swrdpfx  11403  pfxpfx  11404  cats1un  11417  swrdccatfn  11420  swrdccatin1  11421  pfxccatin12lem4  11422  pfxccatin12lem1  11424  swrdccatin2  11425  pfxccatin12lem2c  11426  pfxccatin12lem2  11427  swrdccat3blem  11435  swrdccatin1d  11439  swrdccatin2d  11440  pfxccatin12d  11441  shftfn  11513  shftval  11514  seq3shft  11527  iser3shft  12035  sumeq1  12044  summodclem3  12070  summodclem2a  12071  isumss  12081  fsumsplit  12097  sumsplitdc  12122  fsum2dlemstep  12124  fisumcom2  12128  fsumparts  12160  explecnv  12195  fprodsplitdc  12286  fprodsplit  12287  fprod2dlemstep  12312  fprodcom2fi  12316  eftlub  12380  divalgmod  12617  bitsval  12633  bitsp1e  12642  bitsp1o  12643  algfx  12753  eucalgcvga  12759  reumodprminv  12955  nnnn0modprm0  12957  ballotfilemfc0  13153  ballotfilemfcc  13154  ennnfonelemex  13182  ennnfonelemhom  13183  ennnfonelemf1  13186  ennnfonelemrn  13187  ctinfomlemom  13195  ctinfom  13196  ctiunctlemudc  13205  ctiunctlemf  13206  elrest  13476  ptex  13494  prdsbasmpt  13510  prdsbasmpt2  13518  pwselbasb  13523  imasaddfnlemg  13544  divsfval  13558  xpscf  13577  grpidvalg  13603  grpidpropdg  13604  grpidd  13613  issgrpd  13642  sgrppropd  13643  ismndd  13667  mndpropd  13670  imasmnd2  13682  imasmnd  13683  ismhm  13691  issubm  13702  imasgrp2  13844  imasgrp  13845  issubg  13907  subginv  13915  isnsg  13936  eqg0el  13963  quselbasg  13964  isghm  13977  resghm2b  13996  conjnmzb  14014  conjnsg  14015  ghmpropd  14017  imasabl  14070  gsumsplit0  14080  isrngd  14114  rngpropd  14116  imasrng  14117  qusrng  14119  dfur2g  14123  srgidmlem  14139  issrgid  14142  ringcl  14174  isringid  14186  isringd  14202  imasring  14225  oppr0g  14242  oppr1g  14243  dvdsrvald  14255  isunitd  14268  unitinvcl  14285  unitinvinv  14286  unitlinv  14288  unitrinv  14289  unitnegcl  14292  dvdsrpropdg  14309  isrhm  14320  isrim0  14323  rhmmul  14326  islring  14354  issubrng  14361  opprsubrngg  14373  issubrg  14383  resrhm2b  14411  rhmpropd  14416  rrgval  14424  aprval  14445  aprap  14449  islmod  14456  lmodprop2d  14513  islssm  14522  islssmg  14523  islssmd  14524  lssats2  14579  ellspsn  14582  ixpsnbasval  14631  islidlm  14644  isridlrng  14647  rspssp  14659  rnglidlmmgm  14661  2idlval  14667  isridl  14669  2idlelb  14670  quscrng  14698  rspsn  14699  zrhval  14782  zrhrhmb  14787  znf1o  14816  psrgrp  14857  mplelbascoe  14864  istopon  14895  eltg  14934  eltg2  14935  eltop  14951  eltop2  14952  eltop3  14953  iscld  14985  neiss2  15024  isnei  15026  lmfval  15075  cnfval  15076  iscn  15079  iscnp  15081  tgcn  15090  tgcnp  15091  lmbrf  15097  cnptopresti  15120  txbas  15140  eltx  15141  txdis  15159  txdis1cn  15160  hmeofvalg  15185  ishmeo  15186  ispsmet  15205  ismet  15226  isxmet  15227  elblps  15272  elbl  15273  elmopn  15328  neibl  15373  metrest  15388  txmetcnp  15400  txmetcn  15401  metcnpd  15402  elcncf  15455  ellimc3apf  15542  limcmpted  15545  cnlimcim  15553  cnlimc  15554  eldvap  15564  dvidsslem  15575  dviaddf  15587  dvimulf  15588  elply  15616  ply1termlem  15624  lgseisenlem3  15962  edgval  16072  edgiedgbg  16077  edgupgren  16153  upgredg  16156  uhgr2edg  16218  umgr2edg1  16221  usgredg2vlem1  16234  usgredg2vlem2  16235  ushgredgedg  16238  ushgredgedgloop  16240  subgruhgredgdm  16282  uhgrspansubgrlem  16288  vtxdgfval  16300  vtxedgfi  16301  vtxdgop  16304  vtxdg0v  16306  vtxdeqd  16308  vtxdfifiun  16309  1loopgrvd0fi  16318  1hevtxdg0fi  16319  1hevtxdg1en  16320  wksfval  16334  iswlk  16335  wlkm  16351  uspgr2wlkeq  16377  wlkreslem  16390  wlkres  16391  istrl  16397  clwwlkg  16405  isclwwlk  16406  clwwlkccatlem  16412  isclwwlkng  16418  clwwlkn0  16420  clwwlknnn  16424  clwwlkext2edg  16434  clwwlknonmpo  16440  clwwlknon  16441  clwwlk0on0  16443  iseupth  16459  eupth2lem3lem3fi  16482  eupth2lem3lem6fi  16483  eupth2lem3lem4fi  16485  eupth2lembfi  16489  bj-sels  16701  pw1map  16786  nninfall  16804  nninfsellemeq  16809