Theorem eleqtrd 2843

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816

This theorem is referenced by:  eleqtrrd  2844  eleqtrid  2847  eleqtrdi  2851  3eltr3d  2855  prel12g  4864  opth1  5480  0nelop  5501  fvelimad  6976  fviss  6986  feldmfvelcdm  7106  tfisi  7880  fnwelem  8156  frrlem8  8318  frrlem10  8320  fprresex  8335  wfrlem17OLD  8365  omeulem1  8620  oeeulem  8639  oeeui  8640  oaabs2  8687  omabs  8689  ercl  8756  erth  8796  ecelqsdm  8827  ordtypelem6  9563  ordtypelem7  9564  cantnfval  9708  cantnfp1lem3  9720  cantnflem4  9732  r1pwss  9824  rankonidlem  9868  rankxplim3  9921  fseqenlem2  10065  iunfictbso  10154  dfac12lem1  10184  dfac12lem2  10185  fin23lem30  10382  iundom2g  10580  fpwwe2lem5  10675  fpwwe2lem8  10678  lincmb01cmp  13535  fzopth  13601  elfzolem1  13744  fzoaddel2  13759  fzosubel2  13764  fzocatel  13768  zpnn0elfzo1  13778  fzoend  13796  fzoopth  13801  peano2fzor  13813  monoord2  14074  sermono  14075  expmulnbnd  14274  bcpasc  14360  hash1elsn  14410  swrdcl  14683  revcl  14799  revlen  14800  fsum0diag2  15819  isumsplit  15876  fprodser  15985  sadadd  16504  sadass  16508  smuval2  16519  smumul  16530  vdwapun  17012  vdwlem9  17027  ramub1lem1  17064  prdsbasfn  17516  prdsbasprj  17517  pwsplusgval  17535  pwsmulrval  17536  pwsvscafval  17539  xpsaddlem  17618  xpsvsca  17622  xpsle  17624  mreexmrid  17686  homfeqval  17740  comfval2  17746  comfeq  17749  comfeqval  17751  oppccomfpropd  17770  invco  17815  sectepi  17828  issubc3  17894  funcf2  17913  fthepi  17975  nat1st2nd  17999  homarcl2  18080  coapm  18116  setcmon  18132  setcepi  18133  setcsect  18134  setcinv  18135  setciso  18136  cat1lem  18141  catccatid  18151  resscatc  18154  catciso  18156  catcbascl  18157  catcoppccl  18162  catcfuccl  18163  xpccatid  18233  catcxpccl  18252  xpcpropd  18253  evlfcl  18267  curfpropd  18278  hofcl  18304  yonedalem3  18325  yonffthlem  18327  poslubdg  18459  grpidd  18684  gsumress  18695  issubmgm2  18716  sgrppropd  18744  ismndd  18769  mndpropd  18772  issubmnd  18774  submnd0  18776  imasmnd  18788  xpsmnd0  18791  frmdelbas  18866  grpidd2  18995  pwsinvg  19071  imasgrp  19074  xpsinv  19078  xpsgrpsub  19079  ressmulgnnd  19096  submmulg  19136  subginvcl  19153  subgcl  19154  subgsub  19156  subgmulg  19158  1nsgtrivd  19192  quseccl0  19203  kerf1ghm  19265  ghmqusnsglem1  19298  ghmquskerlem1  19301  ghmquskerco  19302  ghmqusker  19305  gaid2  19321  finodsubmsubg  19585  submod  19587  odsubdvds  19589  sylow1lem4  19619  sylow2alem2  19636  lsmdisj2  19700  subgdisj1  19709  pj1id  19717  efgsrel  19752  efgrelexlemb  19768  efgcpbl2  19775  frgpcpbl  19777  frgp0  19778  frgpeccl  19779  frgpadd  19781  frgpup3lem  19795  frgpnabllem1  19891  cycsubgcyg  19919  prdsgsum  19999  dprdfeq0  20042  dmdprdsplitlem  20057  dpjidcl  20078  pgpfac1lem3a  20096  pgpfac1lem4  20098  pgpfaclem1  20101  pgpfaclem2  20102  ablfaclem2  20106  simpgnsgeqd  20121  simpgnsgbid  20123  ablsimpnosubgd  20124  rngpropd  20171  imasrng  20174  ringurd  20182  ringidss  20274  ringpropd  20285  imasring  20327  xpsring1d  20330  qusring2  20331  lringuplu  20544  subrngmcl  20557  subrg1  20582  subrgdv  20589  subrgunit  20590  resrhm  20601  issubdrg  20781  lmodprop2d  20922  0lmhm  21039  lmhmpropd  21072  lspfixed  21130  lssacsex  21146  lbsextlem4  21163  quscrng  21293  qusmulcrng  21294  rhmqusnsg  21295  rngqiprngimf  21307  rngqiprngimfo  21311  rngqiprngfulem4  21324  znf1o  21570  freshmansdream  21593  psgnghm2  21599  elocv  21686  pjff  21732  frlmlss  21771  frlmsubgval  21785  frlmvscafval  21786  frlmvscavalb  21790  frlmvplusgscavalb  21791  frlmphl  21801  uvcresum  21813  frlmssuvc1  21814  frlmssuvc2  21815  frlmsslsp  21816  frlmup1  21818  sraassab  21888  assapropd  21892  psrelbas  21954  resspsrvsca  21997  subrgpsr  21998  psrascl  21999  mplcoe1  22055  mplbas2  22060  mplascl  22088  mplmon2cl  22092  mplmon2mul  22093  evlrhm  22120  mpfconst  22125  mhprcl  22147  mhpvscacl  22158  psdascl  22172  vr1cl2  22194  ply1lss  22198  ply1subrg  22199  psropprmul  22239  ply1chr  22310  evl1vsd  22348  evl1expd  22349  evl1gsumadd  22362  evl1gsummon  22369  evls1fpws  22373  evls1vsca  22377  asclply1subcl  22378  evls1maplmhm  22381  evl1maprhm  22383  ply1vscl  22388  matring  22449  matassa  22450  mat1  22453  mattposcl  22459  mavmulass  22555  mdetunilem9  22626  matinv  22683  cpmadugsumlemF  22882  cpmadugsumfi  22883  cpmidgsum2  22885  elcls3  23091  mreclatdemoBAD  23104  neiptopnei  23140  resstps  23195  ordtrest2lem  23211  ordtrest2  23212  pnfnei  23228  mnfnei  23229  iscnp2  23247  iscnp4  23271  cnrest2r  23295  lmcls  23310  lmcld  23311  cnt0  23354  cnhaus  23362  isreg2  23385  connclo  23423  1stccnp  23470  loclly  23495  lly1stc  23504  locfincmp  23534  unisngl  23535  comppfsc  23540  kgencmp2  23554  llycmpkgen2  23558  kgen2ss  23563  kgencn3  23566  pttoponconst  23605  txcls  23612  txbasval  23614  dfac14lem  23625  ptcn  23635  ptrescn  23647  txtube  23648  txcmplem1  23649  txlm  23656  txkgen  23660  xkopjcn  23664  cnmptkp  23688  xkoinjcn  23695  qtopkgen  23718  imastps  23729  isr0  23745  r0cld  23746  pt1hmeo  23814  ptuncnv  23815  ptunhmeo  23816  filintn0  23869  trnei  23900  flimfil  23977  flimopn  23983  fbflim2  23985  cnpflf2  24008  flfcnp  24012  flfcnp2  24015  fclsopn  24022  fcfnei  24043  cnpfcf  24049  flfcntr  24051  alexsublem  24052  ptcmplem3  24062  ptcmplem4  24063  cnextfres1  24076  tmdcn2  24097  tmdgsum  24103  tmdgsum2  24104  efmndtmd  24109  symgtgp  24114  tgphaus  24125  tgpt1  24126  qustgplem  24129  prdstmdd  24132  prdstgpd  24133  haustsms  24144  tsmscls  24146  tsmsmhm  24154  tsmsadd  24155  tgptsmscls  24158  tsmssplit  24160  restutop  24246  utopreg  24261  ressusp  24273  ucncn  24294  xmetunirn  24347  ressprdsds  24381  xpsdsval  24391  xblss2ps  24411  blbas  24440  mopntopon  24449  isxms2  24458  imasf1oxms  24502  imasf1oms  24503  prdsxmslem2  24542  tmsxpsval  24551  tngngp2  24673  tngngp  24675  tgioo  24817  metdseq0  24876  cncfmpt2f  24941  cncfcnvcn  24952  cnmptre  24954  cnheibor  24987  nmhmcn  25153  cvsdiv  25165  cvsdivcl  25166  cphsubrglem  25211  cphreccllem  25212  iscmet3  25327  relcmpcmet  25352  bcthlem4  25361  rrxds  25427  rrxvsca  25428  rrxplusgvscavalb  25429  rrxbasefi  25444  rrxmetfi  25446  minveclem4  25466  mulcncf  25480  ivthicc  25493  evthicc  25494  ovolicc2lem4  25555  ovolicc2lem5  25556  iunmbl2  25592  vitalilem3  25645  cncombf  25693  cnmbf  25694  dvres2lem  25945  cpncn  25972  cpnres  25973  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  dvcjbr  25987  dvrec  25993  dvcnvlem  26014  dvlip2  26034  dvivth  26049  lhop2  26054  lhop  26055  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcnvre  26058  ftc1lem6  26082  mdegvscale  26114  mdegvsca  26115  fta1blem  26210  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  tayl0  26403  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmdvlem3  26445  psercnlem2  26468  psercn  26470  efsubm  26593  cxpcn3  26791  loglesqrt  26804  efrlim  27012  efrlimOLD  27013  ppinprm  27195  chtnprm  27197  dchrptlem1  27308  dchrptlem2  27309  nodenselem5  27733  oldlim  27925  cofcutr  27958  addsproplem6  28007  negsproplem6  28065  mulsproplem13  28154  mulsproplem14  28155  noseqp1  28297  tgbtwnouttr2  28503  tgldim0eq  28511  tgifscgr  28516  iscgrglt  28522  ercgrg  28525  tgcgrxfr  28526  motcgrg  28552  tglngne  28558  tgcolg  28562  tgbtwnconn1lem2  28581  tgbtwnconn1lem3  28582  legtri3  28598  legbtwn  28602  ncolne1  28633  tgisline  28635  tglinethru  28644  coltr3  28656  colline  28657  tglowdim2ln  28659  mirinv  28674  miriso  28678  mirauto  28692  miduniq  28693  krippenlem  28698  midexlem  28700  ragperp  28725  footexALT  28726  footexlem2  28728  perpdragALT  28735  perpdrag  28736  colperpexlem1  28738  colperpexlem3  28740  mideulem2  28742  midex  28745  opphllem1  28755  opphllem3  28757  opphllem4  28758  hlpasch  28764  trgcopy  28812  f1otrg  28879  axlowdimlem16  28972  elntg  28999  eengtrkg  29001  eengtrkge  29002  clwwlkccatlem  30008  grpoidinv2  30534  grpoinv  30544  ubthlem2  30890  shuni  31319  acunirnmpt  32669  acunirnmpt2  32670  acunirnmpt2f  32671  fpwrelmap  32744  fzm1ne1  32790  fzom1ne1  32803  ccatf1  32933  swrdf1  32941  pfxchn  32999  chnind  33001  chnub  33002  subgmulgcld  33048  gsummpt2d  33052  gsumhashmul  33064  gsumwrd2dccatlem  33069  gsumwrd2dccat  33070  odpmco  33106  pmtrcnel  33109  pmtrcnel2  33110  pmtrcnelor  33111  tocyc01  33138  trsp2cyc  33143  cycpmco2f1  33144  cycpmco2rn  33145  cycpmco2lem1  33146  cycpmco2lem2  33147  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmco2  33153  cycpmconjv  33162  cycpmrn  33163  tocyccntz  33164  0ringcring  33256  rloccring  33274  rloc0g  33275  rloc1r  33276  isdrng4  33298  sdrgdvcl  33301  sdrginvcl  33302  fracfld  33310  lpirlidllpi  33402  pidlnz  33404  nsgmgc  33440  rhmquskerlem  33453  elrspunidl  33456  elrspunsn  33457  drngidl  33461  qsidomlem1  33480  mxidlirred  33500  drngmxidlr  33506  opprmxidlabs  33515  opprqusplusg  33517  opprqusmulr  33519  opprqusdrng  33521  qsdrngilem  33522  qsdrngi  33523  qsdrnglem2  33524  qsdrng  33525  qsfld  33526  idlsrg0g  33534  1arithidomlem2  33564  ressdeg1  33591  ressply1invg  33594  ressply1sub  33595  ressasclcl  33596  ply1degltlss  33617  gsummoncoe1fzo  33618  ig1pmindeg  33622  q1pvsca  33624  r1pvsca  33625  srasubrg  33635  drgextlsp  33644  matdim  33666  lbslsat  33667  ply1degltdimlem  33673  ply1degltdim  33674  lindsunlem  33675  lbsdiflsp0  33677  dimkerim  33678  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  fldexttr  33709  extdgmul  33714  extdg1id  33716  irngss  33737  irngnzply1lem  33740  irngnzply1  33741  irngnminplynz  33755  algextdeglem4  33761  algextdeglem8  33765  rtelextdg2lem  33767  rtelextdg2  33768  constrconj  33786  rspectopn  33866  zarclsiin  33870  zarmxt1  33879  rspectps  33882  rhmpreimacn  33884  ordtrest2NEWlem  33921  ordtrest2NEW  33922  lmxrge0  33951  nmmulg  33967  rrhcn  33998  esumadd  34058  esumaddf  34062  esumcocn  34081  measiuns  34218  mbfmco2  34267  dya2iocnrect  34283  omscl  34297  omsf  34298  oms0  34299  sibf0  34336  sibfof  34342  sitgaddlemb  34350  fibp1  34403  ccatmulgnn0dir  34557  cxpcncf1  34610  ftc2re  34613  fsum2dsub  34622  reprf  34627  reprsum  34628  bnj1450  35064  bnj1501  35081  revpfxsfxrev  35121  indispconn  35239  connpconn  35240  pconnpi1  35242  sconnpi1  35244  cvmsss2  35279  cvmliftmolem1  35286  cvmliftlem8  35297  cvmliftlem10  35299  cvmliftlem11  35300  cvmlift2lem9  35316  cvmlift2lem12  35319  cvmlift3lem7  35330  mrsubcv  35515  mrsubff  35517  mrsubccat  35523  elmrsubrn  35525  mrsubco  35526  mrsubvrs  35527  linethru  36154  ivthALT  36336  neibastop2  36362  filnetlem4  36382  weiunfr  36468  matunitlindflem2  37624  poimirlem1  37628  poimirlem2  37629  poimirlem8  37635  poimirlem9  37636  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimir  37660  broucube  37661  areacirclem4  37718  fdc  37752  isbnd3  37791  prdsbnd  37800  prdstotbnd  37801  prdsbnd2  37802  rrnequiv  37842  reheibor  37846  iscringd  38005  isfldidl  38075  eqvrelth  38612  eqlkr  39100  ldualvsubval  39158  dvalveclem  41027  dia2dimlem5  41070  dia2dimlem9  41074  tendoinvcl  41106  dvhgrp  41109  dvhlveclem  41110  dihpN  41338  dochsnkr2cl  41476  lcfl7lem  41501  lclkr  41535  lclkrs  41541  lcfrvalsnN  41543  lcfrlem4  41547  lcfrlem6  41549  lcfrlem16  41560  lcdvsubval  41620  lcdlkreqN  41624  mapdcl2  41658  mapdincl  41663  mapdlsmcl  41665  mapdpglem3  41677  hdmaprnlem9N  41859  hdmaplkr  41915  hdmapip0  41917  hdmapglem7a  41929  zndvdchrrhm  41972  remexz  42105  primrootspoweq0  42107  aks6d1c1p3  42111  aks6d1c1p5  42113  aks6d1c2lem4  42128  idomnnzpownz  42133  idomnnzgmulnz  42134  ringexp0nn  42135  aks6d1c5lem0  42136  aks6d1c5lem3  42138  aks6d1c5lem2  42139  aks6d1c5  42140  sticksstones11  42157  sticksstones12a  42158  sticksstones19  42166  aks6d1c6lem2  42172  aks6d1c6lem4  42174  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  aks6d1c6lem5  42178  aks5lem2  42188  ply1asclzrhval  42189  rhmpsr1  42563  evlsscaval  42574  selvvvval  42595  evlselv  42597  mhphf2  42608  mhphf4  42610  prjspnvs  42630  prjspnn0  42632  prjspner1  42636  fltnltalem  42672  diophin  42783  acongeq  42995  isnumbasgrplem2  43116  proot1mul  43206  oacl2g  43343  omabs2  43345  omcl2  43346  iunrelexpuztr  43732  ntrclsiex  44066  ntrneiiex  44089  ntrneinex  44090  elnelneqd  44215  grurankcld  44252  bccbc  44364  suctrALT  44846  restuni3  45123  disjf1o  45196  disjinfi  45197  choicefi  45205  fsneq  45211  fsneqrn  45216  unirnmapsn  45219  iunmapsn  45222  monoords  45309  uzfissfz  45337  monoord2xrv  45494  evthiccabs  45509  iooabslt  45512  tgqioo2  45560  islptre  45634  limciccioolb  45636  sumnnodd  45645  limcicciooub  45652  lptre2pt  45655  limcresiooub  45657  limcresioolb  45658  lptioo1cn  45661  reclimc  45668  liminfvalxr  45798  liminfvaluz  45807  limsupvaluz3  45813  fsumcncf  45893  ioccncflimc  45900  cncfuni  45901  icccncfext  45902  cncficcgt0  45903  icocncflimc  45904  cncfdmsn  45905  cncfiooicclem1  45908  cncfiooicc  45909  cncfioobd  45912  cxpcncf2  45914  fprodsub2cncf  45920  fprodadd2cncf  45921  fperdvper  45934  dvcosax  45941  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  itgsubsticclem  45990  fvvolioof  46004  fvvolicof  46006  stoweidlem26  46041  stoweidlem27  46042  stoweidlem31  46046  stoweidlem34  46049  dirkercncflem2  46119  dirkercncflem3  46120  dirkercncflem4  46121  dirkercncf  46122  fourierdlem16  46138  fourierdlem20  46142  fourierdlem21  46143  fourierdlem22  46144  fourierdlem26  46148  fourierdlem32  46154  fourierdlem33  46155  fourierdlem38  46160  fourierdlem39  46161  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem53  46174  fourierdlem60  46181  fourierdlem61  46182  fourierdlem69  46190  fourierdlem70  46191  fourierdlem71  46192  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem80  46201  fourierdlem81  46202  fourierdlem82  46203  fourierdlem83  46204  fourierdlem84  46205  fourierdlem85  46206  fourierdlem88  46209  fourierdlem89  46210  fourierdlem91  46212  fourierdlem92  46213  fourierdlem93  46214  fourierdlem100  46221  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fouriersw  46246  fouriercn  46247  etransclem24  46273  etransclem26  46275  etransclem28  46277  etransclem31  46280  etransclem32  46281  etransclem33  46282  etransclem34  46283  etransclem35  46284  etransclem38  46287  rrxtopnfi  46302  rrxtoponfi  46306  qndenserrnbl  46310  qndenserrnopnlem  46312  qndenserrn  46314  rrnprjdstle  46316  ioorrnopnlem  46319  prsal  46333  intsaluni  46344  salgencntex  46358  subsaliuncllem  46372  fge0iccico  46385  sge0sn  46394  sge0tsms  46395  sge0cl  46396  sge0f1o  46397  sge0pr  46409  sge0isum  46442  nnfoctbdjlem  46470  iundjiunlem  46474  iundjiun  46475  meadjiunlem  46480  psmeasure  46486  meaiininclem  46501  caragenelss  46516  omeunile  46520  carageniuncllem1  46536  carageniuncllem2  46537  0ome  46544  isomenndlem  46545  isomennd  46546  hoicvr  46563  ovnpnfelsup  46574  ovncvrrp  46579  ovnsubaddlem1  46585  hoidmv1le  46609  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvle  46615  ovnhoilem1  46616  hoi2toco  46622  ovncvr2  46626  hspdifhsp  46631  voncmpl  46636  hoiqssbl  46640  hspmbllem2  46642  hspmbl  46644  hoimbllem  46645  opnvonmbllem2  46648  mblvon  46654  ovolval3  46662  ovolval4lem1  46664  ovnovollem1  46671  ovnovollem2  46672  vonsn  46706  issmflem  46742  sssmf  46753  issmflelem  46759  issmfgtlem  46770  issmfgt  46771  smfaddlem1  46778  issmfgelem  46784  smflimlem3  46788  smfmullem2  46807  smfmullem4  46809  smfsuplem1  46826  smfsupmpt  46830  smfinfmpt  46834  smflimsuplem2  46836  smflimsuplem4  46838  smflimsupmpt  46844  smfliminfmpt  46847  fsupdm  46857  finfdm  46861  ormkglobd  46890  difltmodne  47344  zlmodzxzel  48271  ply1mulgsum  48307  catprs  48900  upeu4  48947  swapf2a  48977  fuco2eld2  49009  fucof21  49042  fucoco2  49053  thincmod  49079  oppcthinco  49088  oppcthinendcALT  49090  termchomn0  49129  termcterm  49145  oduoppcciso  49170  mndtcob  49179  mndtccatid  49184  mndtcid  49186  grptcmon  49190  grptcepi  49191