Theorem eleqtrd 2840

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 2823	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 231	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-clel 2814

This theorem is referenced by:  eleqtrrd  2841  eleqtrid  2844  eleqtrdi  2848  3eltr3d  2852  prel12g  4819  opth1  5430  0nelop  5451  fvelimad  6906  fviss  6915  tfisi  7787  fnwelem  8055  frrlem8  8216  frrlem10  8218  fprresex  8233  wfrlem17OLD  8263  omeulem1  8521  oeeulem  8540  oeeui  8541  oaabs2  8587  omabs  8589  ercl  8617  erth  8655  ecelqsdm  8684  ordtypelem6  9417  ordtypelem7  9418  cantnfval  9562  cantnfp1lem3  9574  cantnflem4  9586  r1pwss  9678  rankonidlem  9722  rankxplim3  9775  fseqenlem2  9919  iunfictbso  10008  dfac12lem1  10037  dfac12lem2  10038  fin23lem30  10236  iundom2g  10434  fpwwe2lem5  10529  fpwwe2lem8  10532  lincmb01cmp  13366  fzopth  13432  fzoaddel2  13582  fzosubel2  13586  fzocatel  13590  zpnn0elfzo1  13600  fzoend  13617  peano2fzor  13633  monoord2  13893  sermono  13894  expmulnbnd  14092  bcpasc  14175  hash1elsn  14225  swrdcl  14487  revcl  14603  revlen  14604  fsum0diag2  15622  isumsplit  15679  fprodser  15786  sadadd  16301  sadass  16305  smuval2  16316  smumul  16327  vdwapun  16800  vdwlem9  16815  ramub1lem1  16852  prdsbasfn  17307  prdsbasprj  17308  pwsplusgval  17326  pwsmulrval  17327  pwsvscafval  17330  xpsaddlem  17409  xpsvsca  17413  xpsle  17415  mreexmrid  17477  homfeqval  17531  comfval2  17537  comfeq  17540  comfeqval  17542  oppccomfpropd  17563  invco  17608  sectepi  17621  issubc3  17689  funcf2  17708  fthepi  17769  nat1st2nd  17792  homarcl2  17875  coapm  17911  setcmon  17927  setcepi  17928  setcsect  17929  setcinv  17930  setciso  17931  cat1lem  17936  catccatid  17946  resscatc  17949  catciso  17951  catcbascl  17952  catcoppccl  17957  catcoppcclOLD  17958  catcfuccl  17959  catcfucclOLD  17960  xpccatid  18030  catcxpccl  18049  catcxpcclOLD  18050  xpcpropd  18051  evlfcl  18065  curfpropd  18076  hofcl  18102  yonedalem3  18123  yonffthlem  18125  poslubdg  18257  grpidd  18480  gsumress  18491  ismndd  18532  mndpropd  18535  issubmnd  18537  submnd0  18539  imasmnd  18548  frmdelbas  18617  grpidd2  18742  pwsinvg  18813  imasgrp  18816  submmulg  18873  subginvcl  18890  subgcl  18891  subgsub  18893  subgmulg  18895  1nsgtrivd  18929  quseccl  18939  gaid2  19036  finodsubmsubg  19302  submod  19304  odsubdvds  19306  sylow1lem4  19336  sylow2alem2  19353  lsmdisj2  19417  subgdisj1  19426  pj1id  19434  efgsrel  19469  efgrelexlemb  19485  efgcpbl2  19492  frgpcpbl  19494  frgp0  19495  frgpeccl  19496  frgpadd  19498  frgpup3lem  19512  frgpnabllem1  19604  cycsubgcyg  19631  prdsgsum  19711  dprdfeq0  19754  dmdprdsplitlem  19769  dpjidcl  19790  pgpfac1lem3a  19808  pgpfac1lem4  19810  pgpfaclem1  19813  pgpfaclem2  19814  ablfaclem2  19818  simpgnsgeqd  19833  simpgnsgbid  19835  ablsimpnosubgd  19836  ringidss  19946  ringpropd  19953  imasring  19992  qusring2  19993  kerf1ghm  20124  subrg1  20179  subrgmcl  20181  subrgdv  20186  subrgunit  20187  issubdrg  20194  resrhm  20198  lmodprop2d  20331  0lmhm  20448  lmhmpropd  20481  lspfixed  20536  lssacsex  20552  lbsextlem4  20569  quscrng  20657  znf1o  20905  psgnghm2  20932  elocv  21019  pjff  21065  frlmlss  21104  frlmsubgval  21118  frlmvscafval  21119  frlmvscavalb  21123  frlmvplusgscavalb  21124  frlmphl  21134  uvcresum  21146  frlmssuvc1  21147  frlmssuvc2  21148  frlmsslsp  21149  frlmup1  21151  assapropd  21222  psrelbas  21294  resspsrvsca  21333  subrgpsr  21334  mplcoe1  21384  mplbas2  21389  mplascl  21418  mplmon2cl  21422  mplmon2mul  21423  evlrhm  21452  mpfconst  21457  mhpvscacl  21490  vr1cl2  21510  ply1lss  21513  ply1subrg  21514  psropprmul  21555  evl1vsd  21656  evl1expd  21657  evl1gsumadd  21670  evl1gsummon  21677  matring  21738  matassa  21739  mat1  21742  mattposcl  21748  mavmulass  21844  mdetunilem9  21915  matinv  21972  cpmadugsumlemF  22171  cpmadugsumfi  22172  cpmidgsum2  22174  elcls3  22380  mreclatdemoBAD  22393  neiptopnei  22429  resstps  22484  ordtrest2lem  22500  ordtrest2  22501  pnfnei  22517  mnfnei  22518  iscnp2  22536  iscnp4  22560  cnrest2r  22584  lmcls  22599  lmcld  22600  cnt0  22643  cnhaus  22651  isreg2  22674  connclo  22712  1stccnp  22759  loclly  22784  lly1stc  22793  locfincmp  22823  unisngl  22824  comppfsc  22829  kgencmp2  22843  llycmpkgen2  22847  kgen2ss  22852  kgencn3  22855  pttoponconst  22894  txcls  22901  txbasval  22903  dfac14lem  22914  ptcn  22924  ptrescn  22936  txtube  22937  txcmplem1  22938  txlm  22945  txkgen  22949  xkopjcn  22953  cnmptkp  22977  xkoinjcn  22984  qtopkgen  23007  imastps  23018  isr0  23034  r0cld  23035  pt1hmeo  23103  ptuncnv  23104  ptunhmeo  23105  filintn0  23158  trnei  23189  flimfil  23266  flimopn  23272  fbflim2  23274  cnpflf2  23297  flfcnp  23301  flfcnp2  23304  fclsopn  23311  fcfnei  23332  cnpfcf  23338  flfcntr  23340  alexsublem  23341  ptcmplem3  23351  ptcmplem4  23352  cnextfres1  23365  tmdcn2  23386  tmdgsum  23392  tmdgsum2  23393  efmndtmd  23398  symgtgp  23403  tgphaus  23414  tgpt1  23415  qustgplem  23418  prdstmdd  23421  prdstgpd  23422  haustsms  23433  tsmscls  23435  tsmsmhm  23443  tsmsadd  23444  tgptsmscls  23447  tsmssplit  23449  restutop  23535  utopreg  23550  ressusp  23562  ucncn  23583  xmetunirn  23636  ressprdsds  23670  xpsdsval  23680  xblss2ps  23700  blbas  23729  mopntopon  23738  isxms2  23747  imasf1oxms  23791  imasf1oms  23792  prdsxmslem2  23831  tmsxpsval  23840  tngngp2  23962  tngngp  23964  tgioo  24105  metdseq0  24163  cncfmpt2f  24224  cncfcnvcn  24234  cnmptre  24236  cnheibor  24264  nmhmcn  24429  cvsdiv  24441  cvsdivcl  24442  cphsubrglem  24487  cphreccllem  24488  iscmet3  24603  relcmpcmet  24628  bcthlem4  24637  rrxds  24703  rrxvsca  24704  rrxplusgvscavalb  24705  rrxbasefi  24720  rrxmetfi  24722  minveclem4  24742  ivthicc  24768  evthicc  24769  ovolicc2lem4  24830  ovolicc2lem5  24831  iunmbl2  24867  vitalilem3  24920  cncombf  24968  cnmbf  24969  dvres2lem  25220  cpncn  25246  cpnres  25247  dvaddbr  25248  dvmulbr  25249  dvcobr  25256  dvcjbr  25259  dvrec  25265  dvcnvlem  25286  dvlip2  25305  dvivth  25320  lhop2  25325  lhop  25326  dvcnvrelem1  25327  dvcnvrelem2  25328  dvcnvre  25329  ftc1lem6  25351  mdegvscale  25386  mdegvsca  25387  fta1blem  25479  plyaddlem1  25520  plymullem1  25521  coeeulem  25531  tayl0  25667  taylthlem1  25678  taylthlem2  25679  ulmdvlem3  25707  psercnlem2  25729  psercn  25731  efsubm  25853  cxpcn3  26047  loglesqrt  26057  efrlim  26265  ppinprm  26447  chtnprm  26449  dchrptlem1  26558  dchrptlem2  26559  nodenselem5  26982  oldlim  27161  cofcutr  27186  tgbtwnouttr2  27282  tgldim0eq  27290  tgifscgr  27295  iscgrglt  27301  ercgrg  27304  tgcgrxfr  27305  motcgrg  27331  tglngne  27337  tgcolg  27341  tgbtwnconn1lem2  27360  tgbtwnconn1lem3  27361  legtri3  27377  legbtwn  27381  ncolne1  27412  tgisline  27414  tglinethru  27423  coltr3  27435  colline  27436  tglowdim2ln  27438  mirinv  27453  miriso  27457  mirauto  27471  miduniq  27472  krippenlem  27477  midexlem  27479  ragperp  27504  footexALT  27505  footexlem2  27507  perpdragALT  27514  perpdrag  27515  colperpexlem1  27517  colperpexlem3  27519  mideulem2  27521  midex  27524  opphllem1  27534  opphllem3  27536  opphllem4  27537  hlpasch  27543  trgcopy  27591  f1otrg  27658  axlowdimlem16  27751  elntg  27778  eengtrkg  27780  eengtrkge  27781  clwwlkccatlem  28778  grpoidinv2  29302  grpoinv  29312  ubthlem2  29658  shuni  30087  acunirnmpt  31420  acunirnmpt2  31421  acunirnmpt2f  31422  fpwrelmap  31492  fzm1ne1  31534  fzom1ne1  31546  ccatf1  31647  swrdf1  31652  gsummpt2d  31733  gsumhashmul  31740  odpmco  31779  pmtrcnel  31782  pmtrcnel2  31783  pmtrcnelor  31784  tocyc01  31809  trsp2cyc  31814  cycpmco2f1  31815  cycpmco2rn  31816  cycpmco2lem1  31817  cycpmco2lem2  31818  cycpmco2lem3  31819  cycpmco2lem4  31820  cycpmco2lem5  31821  cycpmco2lem6  31822  cycpmco2lem7  31823  cycpmco2  31824  cycpmconjv  31833  cycpmrn  31834  tocyccntz  31835  rngurd  31907  freshmansdream  31909  sdrgdvcl  31918  sdrginvcl  31919  pidlnz  32006  nsgmgc  32032  elrspunidl  32041  qsidomlem1  32063  idlsrg0g  32086  evls1fpws  32108  ressdeg1  32111  ressply1invg  32115  ressply1sub  32116  asclply1subcl  32117  ply1chr  32118  srasubrg  32124  drgextlsp  32131  matdim  32148  lbslsat  32149  lindsunlem  32155  lbsdiflsp0  32157  dimkerim  32158  fedgmullem1  32160  fedgmullem2  32161  fedgmul  32162  fldexttr  32183  extdgmul  32186  extdg1id  32188  irngss  32197  irngnzply1lem  32200  irngnzply1  32201  rspectopn  32276  zarclsiin  32280  zarmxt1  32289  rspectps  32292  rhmpreimacn  32294  ordtrest2NEWlem  32331  ordtrest2NEW  32332  lmxrge0  32361  nmmulg  32377  rrhcn  32406  esumadd  32484  esumaddf  32488  esumcocn  32507  measiuns  32644  mbfmco2  32693  dya2iocnrect  32709  omscl  32723  omsf  32724  oms0  32725  sibf0  32762  sibfof  32768  sitgaddlemb  32776  fibp1  32829  ccatmulgnn0dir  32982  cxpcncf1  33036  ftc2re  33039  fsum2dsub  33048  reprf  33053  reprsum  33054  bnj1450  33490  bnj1501  33507  revpfxsfxrev  33537  indispconn  33656  connpconn  33657  pconnpi1  33659  sconnpi1  33661  cvmsss2  33696  cvmliftmolem1  33703  cvmliftlem8  33714  cvmliftlem10  33716  cvmliftlem11  33717  cvmlift2lem9  33733  cvmlift2lem12  33736  cvmlift3lem7  33747  mrsubcv  33932  mrsubff  33934  mrsubccat  33940  elmrsubrn  33942  mrsubco  33943  mrsubvrs  33944  addsproplem6  34283  negsproplem6  34320  linethru  34670  ivthALT  34739  neibastop2  34765  filnetlem4  34785  matunitlindflem2  36007  poimirlem1  36011  poimirlem2  36012  poimirlem8  36018  poimirlem9  36019  poimirlem16  36026  poimirlem17  36027  poimirlem19  36029  poimirlem20  36030  poimirlem22  36032  poimirlem23  36033  poimir  36043  broucube  36044  areacirclem4  36101  fdc  36136  isbnd3  36175  prdsbnd  36184  prdstotbnd  36185  prdsbnd2  36186  rrnequiv  36226  reheibor  36230  iscringd  36389  isfldidl  36459  eqvrelth  37005  eqlkr  37493  ldualvsubval  37551  dvalveclem  39420  dia2dimlem5  39463  dia2dimlem9  39467  tendoinvcl  39499  dvhgrp  39502  dvhlveclem  39503  dihpN  39731  dochsnkr2cl  39869  lcfl7lem  39894  lclkr  39928  lclkrs  39934  lcfrvalsnN  39936  lcfrlem4  39940  lcfrlem6  39942  lcfrlem16  39953  lcdvsubval  40013  lcdlkreqN  40017  mapdcl2  40051  mapdincl  40056  mapdlsmcl  40058  mapdpglem3  40070  hdmaprnlem9N  40252  hdmaplkr  40308  hdmapip0  40310  hdmapglem7a  40322  sticksstones11  40496  sticksstones12a  40497  sticksstones19  40505  evlsscaval  40662  mhphf  40674  mhphf2  40675  mhphf4  40677  prjspnvs  40861  prjspnn0  40863  prjspner1  40867  fltnltalem  40903  diophin  40998  acongeq  41210  isnumbasgrplem2  41334  proot1mul  41429  oacl2g  41565  omabs2  41566  omcl2  41567  iunrelexpuztr  41896  ntrclsiex  42230  ntrneiiex  42253  ntrneinex  42254  elnelneqd  42380  grurankcld  42418  bccbc  42530  suctrALT  43013  restuni3  43233  disjf1o  43309  disjinfi  43311  choicefi  43320  fsneq  43326  fsneqrn  43331  unirnmapsn  43334  iunmapsn  43337  monoords  43430  elfzolem1  43454  uzfissfz  43459  monoord2xrv  43618  evthiccabs  43629  iooabslt  43632  tgqioo2  43680  islptre  43755  limciccioolb  43757  sumnnodd  43766  limcicciooub  43773  lptre2pt  43776  limcresiooub  43778  limcresioolb  43779  lptioo1cn  43782  reclimc  43789  liminfvalxr  43919  liminfvaluz  43928  limsupvaluz3  43934  fsumcncf  44014  ioccncflimc  44021  cncfuni  44022  icccncfext  44023  cncficcgt0  44024  icocncflimc  44025  cncfdmsn  44026  cncfiooicclem1  44029  cncfiooicc  44030  cncfioobd  44033  cxpcncf2  44035  fprodsub2cncf  44041  fprodadd2cncf  44042  fperdvper  44055  dvcosax  44062  dvnmul  44079  dvnprodlem1  44082  dvnprodlem2  44083  itgsubsticclem  44111  fvvolioof  44125  fvvolicof  44127  stoweidlem26  44162  stoweidlem27  44163  stoweidlem31  44167  stoweidlem34  44170  dirkercncflem2  44240  dirkercncflem3  44241  dirkercncflem4  44242  dirkercncf  44243  fourierdlem16  44259  fourierdlem20  44263  fourierdlem21  44264  fourierdlem22  44265  fourierdlem26  44269  fourierdlem32  44275  fourierdlem33  44276  fourierdlem38  44281  fourierdlem39  44282  fourierdlem46  44288  fourierdlem48  44290  fourierdlem49  44291  fourierdlem53  44295  fourierdlem60  44302  fourierdlem61  44303  fourierdlem69  44311  fourierdlem70  44312  fourierdlem71  44313  fourierdlem73  44315  fourierdlem74  44316  fourierdlem75  44317  fourierdlem76  44318  fourierdlem80  44322  fourierdlem81  44323  fourierdlem82  44324  fourierdlem83  44325  fourierdlem84  44326  fourierdlem85  44327  fourierdlem88  44330  fourierdlem89  44331  fourierdlem91  44333  fourierdlem92  44334  fourierdlem93  44335  fourierdlem100  44342  fourierdlem101  44343  fourierdlem103  44345  fourierdlem104  44346  fourierdlem107  44349  fourierdlem111  44353  fourierdlem112  44354  fourierdlem113  44355  fouriersw  44367  fouriercn  44368  etransclem24  44394  etransclem26  44396  etransclem28  44398  etransclem31  44401  etransclem32  44402  etransclem33  44403  etransclem34  44404  etransclem35  44405  etransclem38  44408  rrxtopnfi  44423  rrxtoponfi  44427  qndenserrnbl  44431  qndenserrnopnlem  44433  qndenserrn  44435  rrnprjdstle  44437  ioorrnopnlem  44440  prsal  44454  intsaluni  44465  salgencntex  44479  subsaliuncllem  44493  fge0iccico  44506  sge0sn  44515  sge0tsms  44516  sge0cl  44517  sge0f1o  44518  sge0pr  44530  sge0isum  44563  nnfoctbdjlem  44591  iundjiunlem  44595  iundjiun  44596  meadjiunlem  44601  psmeasure  44607  meaiininclem  44622  caragenelss  44637  omeunile  44641  carageniuncllem1  44657  carageniuncllem2  44658  0ome  44665  isomenndlem  44666  isomennd  44667  hoicvr  44684  ovnpnfelsup  44695  ovncvrrp  44700  ovnsubaddlem1  44706  hoidmv1le  44730  hoidmvlelem2  44732  hoidmvlelem3  44733  hoidmvlelem4  44734  hoidmvle  44736  ovnhoilem1  44737  hoi2toco  44743  ovncvr2  44747  hspdifhsp  44752  voncmpl  44757  hoiqssbl  44761  hspmbllem2  44763  hspmbl  44765  hoimbllem  44766  opnvonmbllem2  44769  mblvon  44775  ovolval3  44783  ovolval4lem1  44785  ovnovollem1  44792  ovnovollem2  44793  vonsn  44827  issmflem  44863  sssmf  44874  issmflelem  44880  issmfgtlem  44891  issmfgt  44892  smfaddlem1  44899  issmfgelem  44905  smflimlem3  44909  smfmullem2  44928  smfmullem4  44930  smfsuplem1  44947  smfsupmpt  44951  smfinfmpt  44955  smflimsuplem2  44957  smflimsuplem4  44959  smflimsupmpt  44965  smfliminfmpt  44968  fsupdm  44978  finfdm  44982  fzoopth  45454  issubmgm2  45979  zlmodzxzel  46326  ply1mulgsum  46366  catprs  46926  thincmod  46946  mndtcob  47003  mndtccatid  47008  mndtcid  47010  grptcmon  47011  grptcepi  47012