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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  eleqtrrd  2841  eleqtrid  2844  eleqtrdi  2848  3eltr3d  2852  prel12g  4868  opth1  5485  0nelop  5505  fvelimad  6975  fviss  6985  feldmfvelcdm  7105  tfisi  7879  fnwelem  8154  frrlem8  8316  frrlem10  8318  fprresex  8333  wfrlem17OLD  8363  omeulem1  8618  oeeulem  8637  oeeui  8638  oaabs2  8685  omabs  8687  ercl  8754  erth  8794  ecelqsdm  8825  ordtypelem6  9560  ordtypelem7  9561  cantnfval  9705  cantnfp1lem3  9717  cantnflem4  9729  r1pwss  9821  rankonidlem  9865  rankxplim3  9918  fseqenlem2  10062  iunfictbso  10151  dfac12lem1  10181  dfac12lem2  10182  fin23lem30  10379  iundom2g  10577  fpwwe2lem5  10672  fpwwe2lem8  10675  lincmb01cmp  13531  fzopth  13597  elfzolem1  13740  fzoaddel2  13755  fzosubel2  13760  fzocatel  13764  zpnn0elfzo1  13774  fzoend  13792  fzoopth  13797  peano2fzor  13809  monoord2  14070  sermono  14071  expmulnbnd  14270  bcpasc  14356  hash1elsn  14406  swrdcl  14679  revcl  14795  revlen  14796  fsum0diag2  15815  isumsplit  15872  fprodser  15981  sadadd  16500  sadass  16504  smuval2  16515  smumul  16526  vdwapun  17007  vdwlem9  17022  ramub1lem1  17059  prdsbasfn  17517  prdsbasprj  17518  pwsplusgval  17536  pwsmulrval  17537  pwsvscafval  17540  xpsaddlem  17619  xpsvsca  17623  xpsle  17625  mreexmrid  17687  homfeqval  17741  comfval2  17747  comfeq  17750  comfeqval  17752  oppccomfpropd  17773  invco  17818  sectepi  17831  issubc3  17899  funcf2  17918  fthepi  17981  nat1st2nd  18005  homarcl2  18088  coapm  18124  setcmon  18140  setcepi  18141  setcsect  18142  setcinv  18143  setciso  18144  cat1lem  18149  catccatid  18159  resscatc  18162  catciso  18164  catcbascl  18165  catcoppccl  18170  catcoppcclOLD  18171  catcfuccl  18172  catcfucclOLD  18173  xpccatid  18243  catcxpccl  18262  catcxpcclOLD  18263  xpcpropd  18264  evlfcl  18278  curfpropd  18289  hofcl  18315  yonedalem3  18336  yonffthlem  18338  poslubdg  18471  grpidd  18696  gsumress  18707  issubmgm2  18728  sgrppropd  18756  ismndd  18781  mndpropd  18784  issubmnd  18786  submnd0  18788  imasmnd  18800  xpsmnd0  18803  frmdelbas  18878  grpidd2  19007  pwsinvg  19083  imasgrp  19086  xpsinv  19090  xpsgrpsub  19091  ressmulgnnd  19108  submmulg  19148  subginvcl  19165  subgcl  19166  subgsub  19168  subgmulg  19170  1nsgtrivd  19204  quseccl0  19215  kerf1ghm  19277  ghmqusnsglem1  19310  ghmquskerlem1  19313  ghmquskerco  19314  ghmqusker  19317  gaid2  19333  finodsubmsubg  19599  submod  19601  odsubdvds  19603  sylow1lem4  19633  sylow2alem2  19650  lsmdisj2  19714  subgdisj1  19723  pj1id  19731  efgsrel  19766  efgrelexlemb  19782  efgcpbl2  19789  frgpcpbl  19791  frgp0  19792  frgpeccl  19793  frgpadd  19795  frgpup3lem  19809  frgpnabllem1  19905  cycsubgcyg  19933  prdsgsum  20013  dprdfeq0  20056  dmdprdsplitlem  20071  dpjidcl  20092  pgpfac1lem3a  20110  pgpfac1lem4  20112  pgpfaclem1  20115  pgpfaclem2  20116  ablfaclem2  20120  simpgnsgeqd  20135  simpgnsgbid  20137  ablsimpnosubgd  20138  rngpropd  20191  imasrng  20194  ringurd  20202  ringidss  20290  ringpropd  20301  imasring  20343  xpsring1d  20346  qusring2  20347  lringuplu  20560  subrngmcl  20573  subrg1  20598  subrgdv  20605  subrgunit  20606  resrhm  20617  issubdrg  20797  lmodprop2d  20938  0lmhm  21056  lmhmpropd  21089  lspfixed  21147  lssacsex  21163  lbsextlem4  21180  quscrng  21310  qusmulcrng  21311  rhmqusnsg  21312  rngqiprngimf  21324  rngqiprngimfo  21328  rngqiprngfulem4  21341  znf1o  21587  freshmansdream  21610  psgnghm2  21616  elocv  21703  pjff  21749  frlmlss  21788  frlmsubgval  21802  frlmvscafval  21803  frlmvscavalb  21807  frlmvplusgscavalb  21808  frlmphl  21818  uvcresum  21830  frlmssuvc1  21831  frlmssuvc2  21832  frlmsslsp  21833  frlmup1  21835  sraassab  21905  assapropd  21909  psrelbas  21971  resspsrvsca  22014  subrgpsr  22015  psrascl  22016  mplcoe1  22072  mplbas2  22077  mplascl  22105  mplmon2cl  22109  mplmon2mul  22110  evlrhm  22137  mpfconst  22142  mhprcl  22164  mhpvscacl  22175  psdascl  22189  vr1cl2  22209  ply1lss  22213  ply1subrg  22214  psropprmul  22254  ply1chr  22325  evl1vsd  22363  evl1expd  22364  evl1gsumadd  22377  evl1gsummon  22384  evls1fpws  22388  evls1vsca  22392  asclply1subcl  22393  evls1maplmhm  22396  evl1maprhm  22398  ply1vscl  22403  matring  22464  matassa  22465  mat1  22468  mattposcl  22474  mavmulass  22570  mdetunilem9  22641  matinv  22698  cpmadugsumlemF  22897  cpmadugsumfi  22898  cpmidgsum2  22900  elcls3  23106  mreclatdemoBAD  23119  neiptopnei  23155  resstps  23210  ordtrest2lem  23226  ordtrest2  23227  pnfnei  23243  mnfnei  23244  iscnp2  23262  iscnp4  23286  cnrest2r  23310  lmcls  23325  lmcld  23326  cnt0  23369  cnhaus  23377  isreg2  23400  connclo  23438  1stccnp  23485  loclly  23510  lly1stc  23519  locfincmp  23549  unisngl  23550  comppfsc  23555  kgencmp2  23569  llycmpkgen2  23573  kgen2ss  23578  kgencn3  23581  pttoponconst  23620  txcls  23627  txbasval  23629  dfac14lem  23640  ptcn  23650  ptrescn  23662  txtube  23663  txcmplem1  23664  txlm  23671  txkgen  23675  xkopjcn  23679  cnmptkp  23703  xkoinjcn  23710  qtopkgen  23733  imastps  23744  isr0  23760  r0cld  23761  pt1hmeo  23829  ptuncnv  23830  ptunhmeo  23831  filintn0  23884  trnei  23915  flimfil  23992  flimopn  23998  fbflim2  24000  cnpflf2  24023  flfcnp  24027  flfcnp2  24030  fclsopn  24037  fcfnei  24058  cnpfcf  24064  flfcntr  24066  alexsublem  24067  ptcmplem3  24077  ptcmplem4  24078  cnextfres1  24091  tmdcn2  24112  tmdgsum  24118  tmdgsum2  24119  efmndtmd  24124  symgtgp  24129  tgphaus  24140  tgpt1  24141  qustgplem  24144  prdstmdd  24147  prdstgpd  24148  haustsms  24159  tsmscls  24161  tsmsmhm  24169  tsmsadd  24170  tgptsmscls  24173  tsmssplit  24175  restutop  24261  utopreg  24276  ressusp  24288  ucncn  24309  xmetunirn  24362  ressprdsds  24396  xpsdsval  24406  xblss2ps  24426  blbas  24455  mopntopon  24464  isxms2  24473  imasf1oxms  24517  imasf1oms  24518  prdsxmslem2  24557  tmsxpsval  24566  tngngp2  24688  tngngp  24690  tgioo  24831  metdseq0  24889  cncfmpt2f  24954  cncfcnvcn  24965  cnmptre  24967  cnheibor  25000  nmhmcn  25166  cvsdiv  25178  cvsdivcl  25179  cphsubrglem  25224  cphreccllem  25225  iscmet3  25340  relcmpcmet  25365  bcthlem4  25374  rrxds  25440  rrxvsca  25441  rrxplusgvscavalb  25442  rrxbasefi  25457  rrxmetfi  25459  minveclem4  25479  mulcncf  25493  ivthicc  25506  evthicc  25507  ovolicc2lem4  25568  ovolicc2lem5  25569  iunmbl2  25605  vitalilem3  25658  cncombf  25706  cnmbf  25707  dvres2lem  25959  cpncn  25986  cpnres  25987  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  dvcjbr  26001  dvrec  26007  dvcnvlem  26028  dvlip2  26048  dvivth  26063  lhop2  26068  lhop  26069  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcnvre  26072  ftc1lem6  26096  mdegvscale  26128  mdegvsca  26129  fta1blem  26224  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  tayl0  26417  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmdvlem3  26459  psercnlem2  26482  psercn  26484  efsubm  26607  cxpcn3  26805  loglesqrt  26818  efrlim  27026  efrlimOLD  27027  ppinprm  27209  chtnprm  27211  dchrptlem1  27322  dchrptlem2  27323  nodenselem5  27747  oldlim  27939  cofcutr  27972  addsproplem6  28021  negsproplem6  28079  mulsproplem13  28168  mulsproplem14  28169  noseqp1  28311  tgbtwnouttr2  28517  tgldim0eq  28525  tgifscgr  28530  iscgrglt  28536  ercgrg  28539  tgcgrxfr  28540  motcgrg  28566  tglngne  28572  tgcolg  28576  tgbtwnconn1lem2  28595  tgbtwnconn1lem3  28596  legtri3  28612  legbtwn  28616  ncolne1  28647  tgisline  28649  tglinethru  28658  coltr3  28670  colline  28671  tglowdim2ln  28673  mirinv  28688  miriso  28692  mirauto  28706  miduniq  28707  krippenlem  28712  midexlem  28714  ragperp  28739  footexALT  28740  footexlem2  28742  perpdragALT  28749  perpdrag  28750  colperpexlem1  28752  colperpexlem3  28754  mideulem2  28756  midex  28759  opphllem1  28769  opphllem3  28771  opphllem4  28772  hlpasch  28778  trgcopy  28826  f1otrg  28893  axlowdimlem16  28986  elntg  29013  eengtrkg  29015  eengtrkge  29016  clwwlkccatlem  30017  grpoidinv2  30543  grpoinv  30553  ubthlem2  30899  shuni  31328  acunirnmpt  32675  acunirnmpt2  32676  acunirnmpt2f  32677  fpwrelmap  32750  fzm1ne1  32796  fzom1ne1  32808  ccatf1  32917  swrdf1  32925  pfxchn  32983  chnind  32984  chnub  32985  subgmulgcld  33030  gsummpt2d  33034  gsumhashmul  33046  gsumwrd2dccatlem  33051  gsumwrd2dccat  33052  odpmco  33088  pmtrcnel  33091  pmtrcnel2  33092  pmtrcnelor  33093  tocyc01  33120  trsp2cyc  33125  cycpmco2f1  33126  cycpmco2rn  33127  cycpmco2lem1  33128  cycpmco2lem2  33129  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  cycpmconjv  33144  cycpmrn  33145  tocyccntz  33146  0ringcring  33238  rloccring  33256  rloc0g  33257  rloc1r  33258  isdrng4  33278  sdrgdvcl  33280  sdrginvcl  33281  fracfld  33289  lpirlidllpi  33381  pidlnz  33383  nsgmgc  33419  rhmquskerlem  33432  elrspunidl  33435  elrspunsn  33436  drngidl  33440  qsidomlem1  33459  mxidlirred  33479  drngmxidlr  33485  opprmxidlabs  33494  opprqusplusg  33496  opprqusmulr  33498  opprqusdrng  33500  qsdrngilem  33501  qsdrngi  33502  qsdrnglem2  33503  qsdrng  33504  qsfld  33505  idlsrg0g  33513  1arithidomlem2  33543  ressdeg1  33570  ressply1invg  33573  ressply1sub  33574  ressasclcl  33575  ply1degltlss  33596  gsummoncoe1fzo  33597  ig1pmindeg  33601  q1pvsca  33603  r1pvsca  33604  srasubrg  33613  drgextlsp  33622  matdim  33642  lbslsat  33643  ply1degltdimlem  33649  ply1degltdim  33650  lindsunlem  33651  lbsdiflsp0  33653  dimkerim  33654  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  fldexttr  33685  extdgmul  33688  extdg1id  33690  irngss  33701  irngnzply1lem  33704  irngnzply1  33705  irngnminplynz  33719  algextdeglem4  33725  algextdeglem8  33729  rtelextdg2lem  33731  rtelextdg2  33732  constrconj  33749  rspectopn  33827  zarclsiin  33831  zarmxt1  33840  rspectps  33843  rhmpreimacn  33845  ordtrest2NEWlem  33882  ordtrest2NEW  33883  lmxrge0  33912  nmmulg  33928  rrhcn  33959  esumadd  34037  esumaddf  34041  esumcocn  34060  measiuns  34197  mbfmco2  34246  dya2iocnrect  34262  omscl  34276  omsf  34277  oms0  34278  sibf0  34315  sibfof  34321  sitgaddlemb  34329  fibp1  34382  ccatmulgnn0dir  34535  cxpcncf1  34588  ftc2re  34591  fsum2dsub  34600  reprf  34605  reprsum  34606  bnj1450  35042  bnj1501  35059  revpfxsfxrev  35099  indispconn  35218  connpconn  35219  pconnpi1  35221  sconnpi1  35223  cvmsss2  35258  cvmliftmolem1  35265  cvmliftlem8  35276  cvmliftlem10  35278  cvmliftlem11  35279  cvmlift2lem9  35295  cvmlift2lem12  35298  cvmlift3lem7  35309  mrsubcv  35494  mrsubff  35496  mrsubccat  35502  elmrsubrn  35504  mrsubco  35505  mrsubvrs  35506  linethru  36134  ivthALT  36317  neibastop2  36343  filnetlem4  36363  weiunfr  36449  matunitlindflem2  37603  poimirlem1  37607  poimirlem2  37608  poimirlem8  37614  poimirlem9  37615  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimir  37639  broucube  37640  areacirclem4  37697  fdc  37731  isbnd3  37770  prdsbnd  37779  prdstotbnd  37780  prdsbnd2  37781  rrnequiv  37821  reheibor  37825  iscringd  37984  isfldidl  38054  eqvrelth  38592  eqlkr  39080  ldualvsubval  39138  dvalveclem  41007  dia2dimlem5  41050  dia2dimlem9  41054  tendoinvcl  41086  dvhgrp  41089  dvhlveclem  41090  dihpN  41318  dochsnkr2cl  41456  lcfl7lem  41481  lclkr  41515  lclkrs  41521  lcfrvalsnN  41523  lcfrlem4  41527  lcfrlem6  41529  lcfrlem16  41540  lcdvsubval  41600  lcdlkreqN  41604  mapdcl2  41638  mapdincl  41643  mapdlsmcl  41645  mapdpglem3  41657  hdmaprnlem9N  41839  hdmaplkr  41895  hdmapip0  41897  hdmapglem7a  41909  zndvdchrrhm  41952  remexz  42085  primrootspoweq0  42087  aks6d1c1p3  42091  aks6d1c1p5  42093  aks6d1c2lem4  42108  idomnnzpownz  42113  idomnnzgmulnz  42114  ringexp0nn  42115  aks6d1c5lem0  42116  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks6d1c5  42120  sticksstones11  42137  sticksstones12a  42138  sticksstones19  42146  aks6d1c6lem2  42152  aks6d1c6lem4  42154  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6lem5  42158  aks5lem2  42168  ply1asclzrhval  42169  rhmpsr1  42539  evlsscaval  42550  selvvvval  42571  evlselv  42573  mhphf2  42584  mhphf4  42586  prjspnvs  42606  prjspnn0  42608  prjspner1  42612  fltnltalem  42648  diophin  42759  acongeq  42971  isnumbasgrplem2  43092  proot1mul  43182  oacl2g  43319  omabs2  43321  omcl2  43322  iunrelexpuztr  43708  ntrclsiex  44042  ntrneiiex  44065  ntrneinex  44066  elnelneqd  44191  grurankcld  44228  bccbc  44340  suctrALT  44823  restuni3  45057  disjf1o  45133  disjinfi  45134  choicefi  45142  fsneq  45148  fsneqrn  45153  unirnmapsn  45156  iunmapsn  45159  monoords  45247  uzfissfz  45275  monoord2xrv  45433  evthiccabs  45448  iooabslt  45451  tgqioo2  45499  islptre  45574  limciccioolb  45576  sumnnodd  45585  limcicciooub  45592  lptre2pt  45595  limcresiooub  45597  limcresioolb  45598  lptioo1cn  45601  reclimc  45608  liminfvalxr  45738  liminfvaluz  45747  limsupvaluz3  45753  fsumcncf  45833  ioccncflimc  45840  cncfuni  45841  icccncfext  45842  cncficcgt0  45843  icocncflimc  45844  cncfdmsn  45845  cncfiooicclem1  45848  cncfiooicc  45849  cncfioobd  45852  cxpcncf2  45854  fprodsub2cncf  45860  fprodadd2cncf  45861  fperdvper  45874  dvcosax  45881  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  itgsubsticclem  45930  fvvolioof  45944  fvvolicof  45946  stoweidlem26  45981  stoweidlem27  45982  stoweidlem31  45986  stoweidlem34  45989  dirkercncflem2  46059  dirkercncflem3  46060  dirkercncflem4  46061  dirkercncf  46062  fourierdlem16  46078  fourierdlem20  46082  fourierdlem21  46083  fourierdlem22  46084  fourierdlem26  46088  fourierdlem32  46094  fourierdlem33  46095  fourierdlem38  46100  fourierdlem39  46101  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem53  46114  fourierdlem60  46121  fourierdlem61  46122  fourierdlem69  46130  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem80  46141  fourierdlem81  46142  fourierdlem82  46143  fourierdlem83  46144  fourierdlem84  46145  fourierdlem85  46146  fourierdlem88  46149  fourierdlem89  46150  fourierdlem91  46152  fourierdlem92  46153  fourierdlem93  46154  fourierdlem100  46161  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem107  46168  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fouriersw  46186  fouriercn  46187  etransclem24  46213  etransclem26  46215  etransclem28  46217  etransclem31  46220  etransclem32  46221  etransclem33  46222  etransclem34  46223  etransclem35  46224  etransclem38  46227  rrxtopnfi  46242  rrxtoponfi  46246  qndenserrnbl  46250  qndenserrnopnlem  46252  qndenserrn  46254  rrnprjdstle  46256  ioorrnopnlem  46259  prsal  46273  intsaluni  46284  salgencntex  46298  subsaliuncllem  46312  fge0iccico  46325  sge0sn  46334  sge0tsms  46335  sge0cl  46336  sge0f1o  46337  sge0pr  46349  sge0isum  46382  nnfoctbdjlem  46410  iundjiunlem  46414  iundjiun  46415  meadjiunlem  46420  psmeasure  46426  meaiininclem  46441  caragenelss  46456  omeunile  46460  carageniuncllem1  46476  carageniuncllem2  46477  0ome  46484  isomenndlem  46485  isomennd  46486  hoicvr  46503  ovnpnfelsup  46514  ovncvrrp  46519  ovnsubaddlem1  46525  hoidmv1le  46549  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hoidmvle  46555  ovnhoilem1  46556  hoi2toco  46562  ovncvr2  46566  hspdifhsp  46571  voncmpl  46576  hoiqssbl  46580  hspmbllem2  46582  hspmbl  46584  hoimbllem  46585  opnvonmbllem2  46588  mblvon  46594  ovolval3  46602  ovolval4lem1  46604  ovnovollem1  46611  ovnovollem2  46612  vonsn  46646  issmflem  46682  sssmf  46693  issmflelem  46699  issmfgtlem  46710  issmfgt  46711  smfaddlem1  46718  issmfgelem  46724  smflimlem3  46728  smfmullem2  46747  smfmullem4  46749  smfsuplem1  46766  smfsupmpt  46770  smfinfmpt  46774  smflimsuplem2  46776  smflimsuplem4  46778  smflimsupmpt  46784  smfliminfmpt  46787  fsupdm  46797  finfdm  46801  difltmodne  47281  zlmodzxzel  48199  ply1mulgsum  48235  catprs  48799  thincmod  48830  oduoppcciso  48881  mndtcob  48890  mndtccatid  48895  mndtcid  48897  grptcmon  48901  grptcepi  48902