Theorem eleqtrd 2917

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eleqtrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eleq2d 2900	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 234	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895

This theorem is referenced by:  eleqtrrd  2918  eleqtrid  2921  eleqtrdi  2925  3eltr3d  2929  prel12g  4796  opth1  5369  0nelop  5388  fvelimad  6734  fviss  6743  tfisi  7575  fnwelem  7827  wfrlem17  7973  omeulem1  8210  oeeulem  8229  oeeui  8230  oaabs2  8274  omabs  8276  ercl  8302  erth  8340  ecelqsdm  8369  ordtypelem6  8989  ordtypelem7  8990  cantnfval  9133  cantnfp1lem3  9145  cantnflem4  9157  r1pwss  9215  rankonidlem  9259  rankxplim3  9312  fseqenlem2  9453  iunfictbso  9542  dfac12lem1  9571  dfac12lem2  9572  fin23lem30  9766  iundom2g  9964  fpwwe2lem6  10059  fpwwe2lem9  10062  lincmb01cmp  12884  fzopth  12947  fzoaddel2  13096  fzosubel2  13100  fzocatel  13104  zpnn0elfzo1  13114  fzoend  13131  peano2fzor  13147  monoord2  13404  sermono  13405  expmulnbnd  13599  bcpasc  13684  hash1elsn  13735  swrdcl  14009  revcl  14125  revlen  14126  fsum0diag2  15140  isumsplit  15197  fprodser  15305  sadadd  15818  sadass  15822  smuval2  15833  smumul  15844  vdwapun  16312  vdwlem9  16327  ramub1lem1  16364  prdsbasfn  16746  prdsbasprj  16747  pwsplusgval  16765  pwsmulrval  16766  pwsvscafval  16769  xpsaddlem  16848  xpsvsca  16852  xpsle  16854  mreexmrid  16916  homfeqval  16969  comfval2  16975  comfeq  16978  comfeqval  16980  oppccomfpropd  16999  invco  17043  sectepi  17056  issubc3  17121  funcf2  17140  fthepi  17200  nat1st2nd  17223  homarcl2  17297  coapm  17333  setcmon  17349  setcepi  17350  setcsect  17351  setcinv  17352  setciso  17353  catccatid  17364  resscatc  17367  catciso  17369  catcoppccl  17370  catcfuccl  17371  xpccatid  17440  catcxpccl  17459  xpcpropd  17460  evlfcl  17474  curfpropd  17485  hofcl  17511  yonedalem3  17532  yonffthlem  17534  poslubdg  17761  grpidd  17883  gsumress  17894  ismndd  17935  mndpropd  17938  issubmnd  17940  submnd0  17942  imasmnd  17951  frmdelbas  18020  grpidd2  18143  pwsinvg  18214  imasgrp  18217  submmulg  18273  subginvcl  18290  subgcl  18291  subgsub  18293  subgmulg  18295  1nsgtrivd  18328  quseccl  18338  gaid2  18435  submod  18696  odsubdvds  18698  sylow1lem4  18728  sylow2alem2  18745  lsmdisj2  18810  subgdisj1  18819  pj1id  18827  efgsrel  18862  efgrelexlemb  18878  efgcpbl2  18885  frgpcpbl  18887  frgp0  18888  frgpeccl  18889  frgpadd  18891  frgpup3lem  18905  frgpnabllem1  18995  cycsubgcyg  19023  prdsgsum  19103  dprdfeq0  19146  dmdprdsplitlem  19161  dpjidcl  19182  pgpfac1lem3a  19200  pgpfac1lem4  19202  pgpfaclem1  19205  pgpfaclem2  19206  ablfaclem2  19210  simpgnsgeqd  19225  simpgnsgbid  19227  ablsimpnosubgd  19228  ringidss  19329  ringpropd  19334  imasring  19371  qusring2  19372  kerf1ghm  19499  kerf1hrmOLD  19500  subrg1  19547  subrgmcl  19549  subrgdv  19554  subrgunit  19555  issubdrg  19562  resrhm  19566  lmodprop2d  19698  0lmhm  19814  lmhmpropd  19847  lspfixed  19902  lssacsex  19918  lbsextlem4  19935  quscrng  20015  assapropd  20103  psrelbas  20161  resspsrvsca  20200  subrgpsr  20201  mplcoe1  20248  mplbas2  20253  mplascl  20278  mplmon2cl  20282  mplmon2mul  20283  evlrhm  20311  mpfconst  20316  mhpvscacl  20343  vr1cl2  20363  ply1lss  20366  ply1subrg  20367  psropprmul  20408  evl1vsd  20509  evl1expd  20510  evl1gsumadd  20523  evl1gsummon  20530  znf1o  20700  psgnghm2  20727  elocv  20814  pjff  20858  frlmlss  20897  frlmsubgval  20911  frlmvscafval  20912  frlmvscavalb  20916  frlmvplusgscavalb  20917  frlmphl  20927  uvcresum  20939  frlmssuvc1  20940  frlmssuvc2  20941  frlmsslsp  20942  frlmup1  20944  matring  21054  matassa  21055  mat1  21058  mattposcl  21064  mavmulass  21160  mdetunilem9  21231  matinv  21288  cpmadugsumlemF  21486  cpmadugsumfi  21487  cpmidgsum2  21489  elcls3  21693  mreclatdemoBAD  21706  neiptopnei  21742  resstps  21797  ordtrest2lem  21813  ordtrest2  21814  pnfnei  21830  mnfnei  21831  iscnp2  21849  iscnp4  21873  cnrest2r  21897  lmcls  21912  lmcld  21913  cnt0  21956  cnhaus  21964  isreg2  21987  connclo  22025  1stccnp  22072  loclly  22097  lly1stc  22106  locfincmp  22136  unisngl  22137  comppfsc  22142  kgencmp2  22156  llycmpkgen2  22160  kgen2ss  22165  kgencn3  22168  pttoponconst  22207  txcls  22214  txbasval  22216  dfac14lem  22227  ptcn  22237  ptrescn  22249  txtube  22250  txcmplem1  22251  txlm  22258  txkgen  22262  xkopjcn  22266  cnmptkp  22290  xkoinjcn  22297  qtopkgen  22320  imastps  22331  isr0  22347  r0cld  22348  pt1hmeo  22416  ptuncnv  22417  ptunhmeo  22418  filintn0  22471  trnei  22502  flimfil  22579  flimopn  22585  fbflim2  22587  cnpflf2  22610  flfcnp  22614  flfcnp2  22617  fclsopn  22624  fcfnei  22645  cnpfcf  22651  flfcntr  22653  alexsublem  22654  ptcmplem3  22664  ptcmplem4  22665  cnextfres1  22678  tmdcn2  22699  tmdgsum  22705  tmdgsum2  22706  efmndtmd  22711  symgtgp  22716  tgphaus  22727  tgpt1  22728  qustgplem  22731  prdstmdd  22734  prdstgpd  22735  haustsms  22746  tsmscls  22748  tsmsmhm  22756  tsmsadd  22757  tgptsmscls  22760  tsmssplit  22762  restutop  22848  utopreg  22863  ressusp  22876  ucncn  22896  xmetunirn  22949  ressprdsds  22983  xpsdsval  22993  xblss2ps  23013  blbas  23042  mopntopon  23051  isxms2  23060  imasf1oxms  23101  imasf1oms  23102  prdsxmslem2  23141  tmsxpsval  23150  tngngp2  23263  tngngp  23265  tgioo  23406  metdseq0  23464  cncfmpt2f  23524  cncfcnvcn  23531  cnmptre  23533  cnheibor  23561  nmhmcn  23726  cvsdiv  23738  cvsdivcl  23739  cphsubrglem  23783  cphreccllem  23784  iscmet3  23898  relcmpcmet  23923  bcthlem4  23932  rrxds  23998  rrxvsca  23999  rrxplusgvscavalb  24000  rrxbasefi  24015  rrxmetfi  24017  minveclem4  24037  ivthicc  24061  evthicc  24062  ovolicc2lem4  24123  ovolicc2lem5  24124  iunmbl2  24160  vitalilem3  24213  cncombf  24261  cnmbf  24262  dvres2lem  24510  cpncn  24535  cpnres  24536  dvaddbr  24537  dvmulbr  24538  dvcobr  24545  dvcjbr  24548  dvrec  24554  dvcnvlem  24575  dvlip2  24594  dvivth  24609  lhop2  24614  lhop  24615  dvcnvrelem1  24616  dvcnvrelem2  24617  dvcnvre  24618  ftc1lem6  24640  mdegvscale  24671  mdegvsca  24672  fta1blem  24764  plyaddlem1  24805  plymullem1  24806  coeeulem  24816  tayl0  24952  taylthlem1  24963  taylthlem2  24964  ulmdvlem3  24992  psercnlem2  25014  psercn  25016  efsubm  25137  cxpcn3  25331  loglesqrt  25341  efrlim  25549  ppinprm  25731  chtnprm  25733  dchrptlem1  25842  dchrptlem2  25843  tgbtwnouttr2  26283  tgldim0eq  26291  tgifscgr  26296  iscgrglt  26302  ercgrg  26305  tgcgrxfr  26306  motcgrg  26332  tglngne  26338  tgcolg  26342  tgbtwnconn1lem2  26361  tgbtwnconn1lem3  26362  legtri3  26378  legbtwn  26382  ncolne1  26413  tgisline  26415  tglinethru  26424  coltr3  26436  colline  26437  tglowdim2ln  26439  mirinv  26454  miriso  26458  mirauto  26472  miduniq  26473  krippenlem  26478  midexlem  26480  ragperp  26505  footexALT  26506  footexlem2  26508  perpdragALT  26515  perpdrag  26516  colperpexlem1  26518  colperpexlem3  26520  mideulem2  26522  midex  26525  opphllem1  26535  opphllem3  26537  opphllem4  26538  hlpasch  26544  trgcopy  26592  f1otrg  26659  axlowdimlem16  26745  elntg  26772  eengtrkg  26774  eengtrkge  26775  clwwlkccatlem  27769  grpoidinv2  28294  grpoinv  28304  ubthlem2  28650  shuni  29079  acunirnmpt  30406  acunirnmpt2  30407  acunirnmpt2f  30408  fpwrelmap  30471  fzm1ne1  30514  fzom1ne1  30526  ccatf1  30627  swrdf1  30632  gsummpt2d  30689  odpmco  30732  pmtrcnel  30735  pmtrcnel2  30736  pmtrcnelor  30737  tocyc01  30762  trsp2cyc  30767  cycpmco2f1  30768  cycpmco2rn  30769  cycpmco2lem1  30770  cycpmco2lem2  30771  cycpmco2lem3  30772  cycpmco2lem4  30773  cycpmco2lem5  30774  cycpmco2lem6  30775  cycpmco2lem7  30776  cycpmco2  30777  cycpmconjv  30786  cycpmrn  30787  tocyccntz  30788  rngurd  30859  freshmansdream  30861  qsidomlem1  30967  srasubrg  30991  drgextlsp  30998  matdim  31015  lbslsat  31016  lindsunlem  31022  lbsdiflsp0  31024  dimkerim  31025  fedgmullem1  31027  fedgmullem2  31028  fedgmul  31029  fldexttr  31050  extdgmul  31053  extdg1id  31055  ordtrest2NEWlem  31167  ordtrest2NEW  31168  lmxrge0  31197  nmmulg  31211  rrhcn  31240  esumadd  31318  esumaddf  31322  esumcocn  31341  measiuns  31478  mbfmco2  31525  dya2iocnrect  31541  omscl  31555  omsf  31556  oms0  31557  sibf0  31594  sibfof  31600  sitgaddlemb  31608  fibp1  31661  ccatmulgnn0dir  31814  cxpcncf1  31868  ftc2re  31871  fsum2dsub  31880  reprf  31885  reprsum  31886  bnj1450  32324  bnj1501  32341  revpfxsfxrev  32364  indispconn  32483  connpconn  32484  pconnpi1  32486  sconnpi1  32488  cvmsss2  32523  cvmliftmolem1  32530  cvmliftlem8  32541  cvmliftlem10  32543  cvmliftlem11  32544  cvmlift2lem9  32560  cvmlift2lem12  32563  cvmlift3lem7  32574  mrsubcv  32759  mrsubff  32761  mrsubccat  32767  elmrsubrn  32769  mrsubco  32770  mrsubvrs  32771  frrlem8  33132  frrlem10  33134  nodenselem5  33194  linethru  33616  ivthALT  33685  neibastop2  33711  filnetlem4  33731  matunitlindflem2  34891  poimirlem1  34895  poimirlem2  34896  poimirlem8  34902  poimirlem9  34903  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem22  34916  poimirlem23  34917  poimir  34927  broucube  34928  areacirclem4  34987  fdc  35022  isbnd3  35064  prdsbnd  35073  prdstotbnd  35074  prdsbnd2  35075  rrnequiv  35115  reheibor  35119  iscringd  35278  isfldidl  35348  eqvrelth  35848  eqlkr  36237  ldualvsubval  36295  dvalveclem  38163  dia2dimlem5  38206  dia2dimlem9  38210  tendoinvcl  38242  dvhgrp  38245  dvhlveclem  38246  dihpN  38474  dochsnkr2cl  38612  lcfl7lem  38637  lclkr  38671  lclkrs  38677  lcfrvalsnN  38679  lcfrlem4  38683  lcfrlem6  38685  lcfrlem16  38696  lcdvsubval  38756  lcdlkreqN  38760  mapdcl2  38794  mapdincl  38799  mapdlsmcl  38801  mapdpglem3  38813  hdmaprnlem9N  38995  hdmaplkr  39051  hdmapip0  39053  hdmapglem7a  39065  fltnltalem  39281  diophin  39376  acongeq  39587  isnumbasgrplem2  39711  proot1mul  39806  iunrelexpuztr  40071  ntrclsiex  40410  ntrneiiex  40433  ntrneinex  40434  elnelneqd  40562  grurankcld  40576  bccbc  40684  suctrALT  41167  restuni3  41391  disjf1o  41459  disjinfi  41461  choicefi  41470  fsneq  41476  fsneqrn  41481  unirnmapsn  41484  iunmapsn  41487  monoords  41571  elfzolem1  41596  uzfissfz  41601  monoord2xrv  41767  evthiccabs  41778  iooabslt  41781  tgqioo2  41830  islptre  41907  limciccioolb  41909  sumnnodd  41918  limcicciooub  41925  lptre2pt  41928  limcresiooub  41930  limcresioolb  41931  lptioo1cn  41934  reclimc  41941  liminfvalxr  42071  liminfvaluz  42080  limsupvaluz3  42086  fsumcncf  42168  ioccncflimc  42175  cncfuni  42176  icccncfext  42177  cncficcgt0  42178  icocncflimc  42179  cncfdmsn  42180  cncfiooicclem1  42183  cncfiooicc  42184  cncfioobd  42187  cxpcncf2  42190  fprodsub2cncf  42196  fprodadd2cncf  42197  fperdvper  42210  dvcosax  42218  dvnmul  42235  dvnprodlem1  42238  dvnprodlem2  42239  itgsubsticclem  42267  fvvolioof  42281  fvvolicof  42283  stoweidlem26  42318  stoweidlem27  42319  stoweidlem31  42323  stoweidlem34  42326  dirkercncflem2  42396  dirkercncflem3  42397  dirkercncflem4  42398  dirkercncf  42399  fourierdlem16  42415  fourierdlem20  42419  fourierdlem21  42420  fourierdlem22  42421  fourierdlem26  42425  fourierdlem32  42431  fourierdlem33  42432  fourierdlem38  42437  fourierdlem39  42438  fourierdlem46  42444  fourierdlem48  42446  fourierdlem49  42447  fourierdlem53  42451  fourierdlem60  42458  fourierdlem61  42459  fourierdlem69  42467  fourierdlem70  42468  fourierdlem71  42469  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem80  42478  fourierdlem81  42479  fourierdlem82  42480  fourierdlem83  42481  fourierdlem84  42482  fourierdlem85  42483  fourierdlem88  42486  fourierdlem89  42487  fourierdlem91  42489  fourierdlem92  42490  fourierdlem93  42491  fourierdlem100  42498  fourierdlem101  42499  fourierdlem103  42501  fourierdlem104  42502  fourierdlem107  42505  fourierdlem111  42509  fourierdlem112  42510  fourierdlem113  42511  fouriersw  42523  fouriercn  42524  etransclem24  42550  etransclem26  42552  etransclem28  42554  etransclem31  42557  etransclem32  42558  etransclem33  42559  etransclem34  42560  etransclem35  42561  etransclem38  42564  rrxtopnfi  42579  rrxtoponfi  42583  qndenserrnbl  42587  qndenserrnopnlem  42589  qndenserrn  42591  rrnprjdstle  42593  ioorrnopnlem  42596  prsal  42610  intsaluni  42619  salgencntex  42633  subsaliuncllem  42647  fge0iccico  42659  sge0sn  42668  sge0tsms  42669  sge0cl  42670  sge0f1o  42671  sge0pr  42683  sge0isum  42716  nnfoctbdjlem  42744  iundjiunlem  42748  iundjiun  42749  meadjiunlem  42754  psmeasure  42760  meaiininclem  42775  caragenelss  42790  omeunile  42794  carageniuncllem1  42810  carageniuncllem2  42811  0ome  42818  isomenndlem  42819  isomennd  42820  hoicvr  42837  ovnpnfelsup  42848  ovncvrrp  42853  ovnsubaddlem1  42859  hoidmv1le  42883  hoidmvlelem2  42885  hoidmvlelem3  42886  hoidmvlelem4  42887  hoidmvle  42889  ovnhoilem1  42890  hoi2toco  42896  ovncvr2  42900  hspdifhsp  42905  voncmpl  42910  hoiqssbl  42914  hspmbllem2  42916  hspmbl  42918  hoimbllem  42919  opnvonmbllem2  42922  mblvon  42928  ovolval3  42936  ovolval4lem1  42938  ovnovollem1  42945  ovnovollem2  42946  vonsn  42980  issmflem  43011  sssmf  43022  issmflelem  43028  issmfgtlem  43039  issmfgt  43040  smfaddlem1  43046  issmfgelem  43052  smflimlem3  43056  smfmullem2  43074  smfmullem4  43076  smfsuplem1  43092  smfsupmpt  43096  smfinfmpt  43100  smflimsuplem2  43102  smflimsuplem4  43104  smflimsupmpt  43110  smfliminfmpt  43113  fzoopth  43534  issubmgm2  44064  zlmodzxzel  44410  ply1mulgsum  44451