Theorem eleqtrd 2887

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

Syntax hints:   → wi 4   = wceq 1637   ∈ wcel 2156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-clel 2802

This theorem is referenced by:  eleqtrrd  2888  syl5eleq  2891  syl6eleq  2895  3eltr3d  2899  prel12g  4586  opth1  5133  0nelop  5149  fviss  6477  tfisi  7288  fnwelem  7526  wfrlem17  7667  omeulem1  7899  oeeulem  7918  oeeui  7919  oaabs2  7962  omabs  7964  ercl  7990  erth  8026  ecelqsdm  8052  ordtypelem6  8667  ordtypelem7  8668  cantnfval  8812  cantnfp1lem3  8824  cantnflem4  8836  r1pwss  8894  rankonidlem  8938  rankxplim3  8991  fseqenlem2  9131  iunfictbso  9220  dfac12lem1  9250  dfac12lem2  9251  fin23lem30  9449  iundom2g  9647  fpwwe2lem6  9742  fpwwe2lem9  9745  lincmb01cmp  12538  fzopth  12601  fzoaddel2  12748  fzosubel2  12752  fzocatel  12756  zpnn0elfzo1  12766  fzoend  12783  peano2fzor  12799  monoord2  13055  sermono  13056  expmulnbnd  13219  bcpasc  13328  swrdcl  13642  revcl  13734  revlen  13735  fsum0diag2  14737  isumsplit  14794  fprodser  14900  sadadd  15408  sadass  15412  smuval2  15423  smumul  15434  vdwapun  15895  vdwlem9  15910  ramub1lem1  15947  prdsbasfn  16336  prdsbasprj  16337  pwsplusgval  16355  pwsmulrval  16356  pwsvscafval  16359  xpsaddlem  16440  xpsvsca  16444  xpsle  16446  mreexmrid  16508  homfeqval  16561  comfval2  16567  comfeq  16570  comfeqval  16572  oppccomfpropd  16591  invco  16635  sectepi  16648  issubc3  16713  funcf2  16732  funciso  16738  fthepi  16792  nat1st2nd  16815  fuciso  16839  homarcl2  16889  coapm  16925  setcmon  16941  setcepi  16942  setcsect  16943  setcinv  16944  setciso  16945  catccatid  16956  resscatc  16959  catciso  16961  catcoppccl  16962  catcfuccl  16963  xpccatid  17033  catcxpccl  17052  xpcpropd  17053  evlfcl  17067  curfpropd  17078  hofcl  17104  yonedalem3  17125  yonffthlem  17127  poslubdg  17354  grpidd  17473  gsumress  17481  ismndd  17518  mndpropd  17521  issubmnd  17523  submnd0  17525  imasmnd  17533  frmdelbas  17595  grpidd2  17664  pwsinvg  17733  imasgrp  17736  submmulg  17788  subginvcl  17805  subgcl  17806  subgsub  17808  subgmulg  17810  quseccl  17852  gaid2  17937  submod  18185  odsubdvds  18187  sylow1lem4  18217  sylow2alem2  18234  lsmdisj2  18296  subgdisj1  18305  pj1id  18313  efgsrel  18348  efgrelexlemb  18364  efgcpbl2  18371  frgpcpbl  18373  frgp0  18374  frgpeccl  18375  frgpadd  18377  frgpup3lem  18391  frgpnabllem1  18477  cycsubgcyg  18503  prdsgsum  18578  dprdfeq0  18623  dmdprdsplitlem  18638  dpjidcl  18659  pgpfac1lem3a  18677  pgpfac1lem4  18679  pgpfaclem1  18682  pgpfaclem2  18683  ablfaclem2  18687  ringidss  18779  ringpropd  18784  imasring  18821  qusring2  18822  kerf1hrm  18947  subrg1  18994  subrgmcl  18996  subrgdv  19001  subrgunit  19002  issubdrg  19009  resrhm  19013  lmodprop2d  19129  0lmhm  19247  lmhmpropd  19280  lspfixed  19335  lspfixedOLD  19336  lssacsex  19352  lbsextlem4  19370  quscrng  19449  assapropd  19536  psrelbas  19588  resspsrvsca  19627  subrgpsr  19628  mplcoe1  19674  mplbas2  19679  mplascl  19704  mplmon2cl  19708  mplmon2mul  19709  evlrhm  19733  mpfconst  19738  vr1cl2  19771  ply1lss  19774  ply1subrg  19775  psropprmul  19816  evl1vsd  19916  evl1expd  19917  evl1gsumadd  19930  evl1gsummon  19937  znf1o  20107  psgnghm2  20134  elocv  20222  pjff  20266  frlmlss  20305  frlmsubgval  20318  frlmvscafval  20319  frlmphl  20330  uvcresum  20342  frlmssuvc1  20343  frlmssuvc2  20344  frlmsslsp  20345  frlmup1  20347  matring  20459  matassa  20460  mat1  20464  mattposcl  20470  mavmulass  20566  mdetunilem9  20637  matinv  20695  cpmadugsumlemF  20894  cpmadugsumfi  20895  cpmidgsum2  20897  elcls3  21101  mreclatdemoBAD  21114  neiptopnei  21150  resstps  21205  ordtrest2lem  21221  ordtrest2  21222  pnfnei  21238  mnfnei  21239  iscnp2  21257  iscnp4  21281  cnrest2r  21305  lmcls  21320  lmcld  21321  cnt0  21364  cnhaus  21372  isreg2  21395  connclo  21432  1stccnp  21479  loclly  21504  lly1stc  21513  locfincmp  21543  unisngl  21544  comppfsc  21549  kgencmp2  21563  llycmpkgen2  21567  kgen2ss  21572  kgencn3  21575  pttoponconst  21614  txcls  21621  txbasval  21623  dfac14lem  21634  ptcn  21644  ptrescn  21656  txtube  21657  txcmplem1  21658  txlm  21665  txkgen  21669  xkopjcn  21673  cnmptkp  21697  xkoinjcn  21704  qtopkgen  21727  imastps  21738  isr0  21754  r0cld  21755  pt1hmeo  21823  ptuncnv  21824  ptunhmeo  21825  filintn0  21878  trnei  21909  flimfil  21986  flimopn  21992  fbflim2  21994  cnpflf2  22017  flfcnp  22021  flfcnp2  22024  fclsopn  22031  fcfnei  22052  cnpfcf  22058  flfcntr  22060  alexsublem  22061  ptcmplem3  22071  ptcmplem4  22072  cnextfres1  22085  tmdcn2  22106  tmdgsum  22112  tmdgsum2  22113  symgtgp  22118  tgphaus  22133  tgpt1  22134  qustgplem  22137  prdstmdd  22140  prdstgpd  22141  haustsms  22152  tsmscls  22154  tsmsmhm  22162  tsmsadd  22163  tgptsmscls  22166  tsmssplit  22168  restutop  22254  utopreg  22269  ressusp  22282  ucncn  22302  xmetunirn  22355  ressprdsds  22389  xpsdsval  22399  xblss2ps  22419  blbas  22448  mopntopon  22457  isxms2  22466  imasf1oxms  22507  imasf1oms  22508  prdsxmslem2  22547  tmsxpsval  22556  tngngp2  22669  tngngp  22671  tgioo  22812  metdseq0  22870  cncfmpt2f  22930  cncfcnvcn  22937  cnmptre  22939  cnheibor  22967  nmhmcn  23132  cvsdiv  23144  cvsdivcl  23145  cphsubrglem  23189  cphreccllem  23190  iscmet3  23303  relcmpcmet  23327  bcthlem4  23336  rrxds  23393  minveclem4  23415  ivthicc  23439  evthicc  23440  ovolicc2lem4  23501  ovolicc2lem5  23502  iunmbl2  23538  vitalilem3  23591  cncombf  23639  cnmbf  23640  dvres2lem  23888  cpncn  23913  cpnres  23914  dvaddbr  23915  dvmulbr  23916  dvcobr  23923  dvcjbr  23926  dvrec  23932  dvcnvlem  23953  dvlip2  23972  dvivth  23987  lhop2  23992  lhop  23993  dvcnvrelem1  23994  dvcnvrelem2  23995  dvcnvre  23996  ftc1lem6  24018  mdegvscale  24049  mdegvsca  24050  fta1blem  24142  plyaddlem1  24183  plymullem1  24184  coeeulem  24194  tayl0  24330  taylthlem1  24341  taylthlem2  24342  ulmdvlem3  24370  psercnlem2  24392  psercn  24394  efsubm  24512  cxpcn3  24703  loglesqrt  24713  efrlim  24910  ppinprm  25092  chtnprm  25094  dchrptlem1  25203  dchrptlem2  25204  tgbtwnouttr2  25604  tgldim0eq  25612  tgifscgr  25617  iscgrglt  25623  ercgrg  25626  tgcgrxfr  25627  motcgrg  25653  tglngne  25659  tgcolg  25663  tgbtwnconn1lem2  25682  tgbtwnconn1lem3  25683  legtri3  25699  legbtwn  25703  ncolne1  25734  tgisline  25736  tglinethru  25745  coltr3  25757  colline  25758  tglowdim2ln  25760  mirinv  25775  miriso  25779  mirauto  25793  miduniq  25794  krippenlem  25799  midexlem  25801  ragperp  25826  footex  25827  perpdragALT  25833  perpdrag  25834  colperpexlem1  25836  colperpexlem3  25838  mideulem2  25840  midex  25843  opphllem1  25853  opphllem3  25855  opphllem4  25856  hlpasch  25862  trgcopy  25910  acopyeu  25939  f1otrg  25965  axlowdimlem16  26051  elntg  26078  eengtrkg  26079  eengtrkge  26080  grpoidinv2  27698  grpoinv  27708  ubthlem2  28055  shuni  28487  acunirnmpt  29786  acunirnmpt2  29787  acunirnmpt2f  29788  fpwrelmap  29835  gsummpt2d  30106  rngurd  30113  ordtrest2NEWlem  30293  ordtrest2NEW  30294  lmxrge0  30323  nmmulg  30337  rrhcn  30366  esumadd  30444  esumaddf  30448  esumcocn  30467  measiuns  30605  mbfmco2  30652  dya2iocnrect  30668  omscl  30682  omsf  30683  oms0  30684  sibf0  30721  sibfof  30727  sitgaddlemb  30735  fibp1  30788  ccatmulgnn0dir  30944  cxpcncf1  30998  ftc2re  31001  fsum2dsub  31010  reprf  31015  reprsum  31016  bnj1450  31441  bnj1501  31458  indispconn  31539  connpconn  31540  pconnpi1  31542  sconnpi1  31544  cvmsss2  31579  cvmliftmolem1  31586  cvmliftlem8  31597  cvmliftlem10  31599  cvmliftlem11  31600  cvmlift2lem9  31616  cvmlift2lem12  31619  cvmlift3lem7  31630  mrsubcv  31730  mrsubff  31732  mrsubccat  31738  elmrsubrn  31740  mrsubco  31741  mrsubvrs  31742  nodenselem5  32159  linethru  32581  ivthALT  32651  neibastop2  32677  filnetlem4  32697  matunitlindflem2  33719  poimirlem1  33723  poimirlem2  33724  poimirlem8  33730  poimirlem9  33731  poimirlem16  33738  poimirlem17  33739  poimirlem19  33741  poimirlem20  33742  poimirlem22  33744  poimirlem23  33745  poimir  33755  broucube  33756  areacirclem4  33815  fdc  33852  isbnd3  33894  prdsbnd  33903  prdstotbnd  33904  prdsbnd2  33905  rrnequiv  33945  reheibor  33949  iscringd  34108  isfldidl  34178  eqlkr  34879  ldualvsubval  34937  dvalveclem  36806  dia2dimlem5  36849  dia2dimlem9  36853  tendoinvcl  36885  dvhgrp  36888  dvhlveclem  36889  dihpN  37117  dochsnkr2cl  37255  lcfl7lem  37280  lclkr  37314  lclkrs  37320  lcfrvalsnN  37322  lcfrlem4  37326  lcfrlem6  37328  lcfrlem16  37339  lcdvsubval  37399  lcdlkreqN  37403  mapdcl2  37437  mapdincl  37442  mapdlsmcl  37444  mapdpglem3  37456  hdmaprnlem9N  37638  hdmaplkr  37694  hdmapip0  37696  hdmapglem7a  37708  diophin  37838  acongeq  38051  isnumbasgrplem2  38175  proot1mul  38278  iunrelexpuztr  38511  ntrclsiex  38851  ntrneiiex  38874  ntrneinex  38875  bccbc  39044  suctrALT  39555  restuni3  39793  disjf1o  39867  disjinfi  39869  choicefi  39879  fsneq  39885  fsneqrn  39890  unirnmapsn  39893  iunmapsn  39896  fvelimad  39942  monoords  39992  elfzolem1  40017  uzfissfz  40022  monoord2xrv  40193  evthiccabs  40202  iooabslt  40205  tgqioo2  40254  islptre  40331  limciccioolb  40333  sumnnodd  40342  limcicciooub  40349  lptre2pt  40352  limcresiooub  40354  limcresioolb  40355  lptioo1cn  40358  reclimc  40365  liminfvalxr  40495  liminfvaluz  40504  limsupvaluz3  40510  fsumcncf  40571  ioccncflimc  40578  cncfuni  40579  icccncfext  40580  cncficcgt0  40581  icocncflimc  40582  cncfdmsn  40583  cncfiooicclem1  40586  cncfiooicc  40587  cncfioobd  40590  cxpcncf2  40593  fprodsub2cncf  40599  fprodadd2cncf  40600  fperdvper  40613  dvcosax  40621  dvnmul  40638  dvnprodlem1  40641  dvnprodlem2  40642  itgsubsticclem  40670  fvvolioof  40685  fvvolicof  40687  stoweidlem26  40722  stoweidlem27  40723  stoweidlem31  40727  stoweidlem34  40730  dirkercncflem2  40800  dirkercncflem3  40801  dirkercncflem4  40802  dirkercncf  40803  fourierdlem16  40819  fourierdlem20  40823  fourierdlem21  40824  fourierdlem22  40825  fourierdlem26  40829  fourierdlem32  40835  fourierdlem33  40836  fourierdlem38  40841  fourierdlem39  40842  fourierdlem46  40848  fourierdlem48  40850  fourierdlem49  40851  fourierdlem53  40855  fourierdlem60  40862  fourierdlem61  40863  fourierdlem69  40871  fourierdlem70  40872  fourierdlem71  40873  fourierdlem73  40875  fourierdlem74  40876  fourierdlem75  40877  fourierdlem76  40878  fourierdlem80  40882  fourierdlem81  40883  fourierdlem82  40884  fourierdlem83  40885  fourierdlem84  40886  fourierdlem85  40887  fourierdlem88  40890  fourierdlem89  40891  fourierdlem91  40893  fourierdlem92  40894  fourierdlem93  40895  fourierdlem100  40902  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  fourierdlem107  40909  fourierdlem111  40913  fourierdlem112  40914  fourierdlem113  40915  fouriersw  40927  fouriercn  40928  etransclem24  40954  etransclem26  40956  etransclem28  40958  etransclem31  40961  etransclem32  40962  etransclem33  40963  etransclem34  40964  etransclem35  40965  etransclem38  40968  rrxbasefi  40982  rrxdsfi  40984  rrxtopnfi  40985  rrxmetfi  40986  rrxtoponfi  40990  qndenserrnbl  40994  qndenserrnopnlem  40996  qndenserrn  40998  rrnprjdstle  41000  ioorrnopnlem  41003  prsal  41017  intsaluni  41026  salgencntex  41040  subsaliuncllem  41054  fge0iccico  41066  sge0sn  41075  sge0tsms  41076  sge0cl  41077  sge0f1o  41078  sge0pr  41090  sge0isum  41123  nnfoctbdjlem  41151  iundjiunlem  41155  iundjiun  41156  meadjiunlem  41161  psmeasure  41167  meaiininclem  41182  caragenelss  41197  omeunile  41201  carageniuncllem1  41217  carageniuncllem2  41218  0ome  41225  isomenndlem  41226  isomennd  41227  hoicvr  41244  ovnpnfelsup  41255  ovncvrrp  41260  ovnsubaddlem1  41266  hoidmv1le  41290  hoidmvlelem2  41292  hoidmvlelem3  41293  hoidmvlelem4  41294  hoidmvle  41296  ovnhoilem1  41297  hoi2toco  41303  ovncvr2  41307  hspdifhsp  41312  voncmpl  41317  hoiqssbl  41321  hspmbllem2  41323  hspmbl  41325  hoimbllem  41326  opnvonmbllem2  41329  mblvon  41335  ovolval3  41343  ovolval4lem1  41345  ovnovollem1  41352  ovnovollem2  41353  vonsn  41387  issmflem  41418  sssmf  41429  issmflelem  41435  issmfgtlem  41446  issmfgt  41447  smfaddlem1  41453  issmfgelem  41459  smflimlem3  41463  smfmullem2  41481  smfmullem4  41483  smfsuplem1  41499  smfsupmpt  41503  smfinfmpt  41507  smflimsuplem2  41509  smflimsuplem4  41511  smflimsupmpt  41517  smfliminfmpt  41520  fzoopth  41912  issubmgm2  42358  zlmodzxzel  42701  ply1mulgsum  42746