Theorem eleqtrd 2827

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802

This theorem is referenced by:  eleqtrrd  2828  eleqtrid  2831  eleqtrdi  2835  3eltr3d  2839  prel12g  4866  opth1  5477  0nelop  5498  fvelimad  6965  fviss  6974  feldmfvelcdm  7095  tfisi  7864  fnwelem  8136  frrlem8  8299  frrlem10  8301  fprresex  8316  wfrlem17OLD  8346  omeulem1  8603  oeeulem  8622  oeeui  8623  oaabs2  8670  omabs  8672  ercl  8736  erth  8775  ecelqsdm  8806  ordtypelem6  9548  ordtypelem7  9549  cantnfval  9693  cantnfp1lem3  9705  cantnflem4  9717  r1pwss  9809  rankonidlem  9853  rankxplim3  9906  fseqenlem2  10050  iunfictbso  10139  dfac12lem1  10168  dfac12lem2  10169  fin23lem30  10367  iundom2g  10565  fpwwe2lem5  10660  fpwwe2lem8  10663  lincmb01cmp  13507  fzopth  13573  fzoaddel2  13723  fzosubel2  13727  fzocatel  13731  zpnn0elfzo1  13741  fzoend  13758  fzoopth  13763  peano2fzor  13775  monoord2  14034  sermono  14035  expmulnbnd  14233  bcpasc  14316  hash1elsn  14366  swrdcl  14631  revcl  14747  revlen  14748  fsum0diag2  15765  isumsplit  15822  fprodser  15929  sadadd  16445  sadass  16449  smuval2  16460  smumul  16471  vdwapun  16946  vdwlem9  16961  ramub1lem1  16998  prdsbasfn  17456  prdsbasprj  17457  pwsplusgval  17475  pwsmulrval  17476  pwsvscafval  17479  xpsaddlem  17558  xpsvsca  17562  xpsle  17564  mreexmrid  17626  homfeqval  17680  comfval2  17686  comfeq  17689  comfeqval  17691  oppccomfpropd  17712  invco  17757  sectepi  17770  issubc3  17838  funcf2  17857  fthepi  17920  nat1st2nd  17944  homarcl2  18027  coapm  18063  setcmon  18079  setcepi  18080  setcsect  18081  setcinv  18082  setciso  18083  cat1lem  18088  catccatid  18098  resscatc  18101  catciso  18103  catcbascl  18104  catcoppccl  18109  catcoppcclOLD  18110  catcfuccl  18111  catcfucclOLD  18112  xpccatid  18182  catcxpccl  18201  catcxpcclOLD  18202  xpcpropd  18203  evlfcl  18217  curfpropd  18228  hofcl  18254  yonedalem3  18275  yonffthlem  18277  poslubdg  18409  grpidd  18634  gsumress  18645  issubmgm2  18666  sgrppropd  18694  ismndd  18719  mndpropd  18722  issubmnd  18724  submnd0  18726  imasmnd  18735  xpsmnd0  18738  frmdelbas  18813  grpidd2  18942  pwsinvg  19017  imasgrp  19020  xpsinv  19024  xpsgrpsub  19025  submmulg  19081  subginvcl  19098  subgcl  19099  subgsub  19101  subgmulg  19103  1nsgtrivd  19137  quseccl0  19148  kerf1ghm  19210  ghmqusnsglem1  19243  ghmquskerlem1  19246  ghmquskerco  19247  ghmqusker  19250  gaid2  19266  finodsubmsubg  19534  submod  19536  odsubdvds  19538  sylow1lem4  19568  sylow2alem2  19585  lsmdisj2  19649  subgdisj1  19658  pj1id  19666  efgsrel  19701  efgrelexlemb  19717  efgcpbl2  19724  frgpcpbl  19726  frgp0  19727  frgpeccl  19728  frgpadd  19730  frgpup3lem  19744  frgpnabllem1  19840  cycsubgcyg  19868  prdsgsum  19948  dprdfeq0  19991  dmdprdsplitlem  20006  dpjidcl  20027  pgpfac1lem3a  20045  pgpfac1lem4  20047  pgpfaclem1  20050  pgpfaclem2  20051  ablfaclem2  20055  simpgnsgeqd  20070  simpgnsgbid  20072  ablsimpnosubgd  20073  rngpropd  20126  imasrng  20129  ringurd  20137  ringidss  20225  ringpropd  20236  imasring  20278  xpsring1d  20281  qusring2  20282  lringuplu  20493  subrngmcl  20506  subrg1  20533  subrgdv  20540  subrgunit  20541  resrhm  20552  issubdrg  20680  lmodprop2d  20819  0lmhm  20937  lmhmpropd  20970  lspfixed  21028  lssacsex  21044  lbsextlem4  21061  quscrng  21190  qusmulcrng  21191  rhmqusnsg  21192  rngqiprngimf  21204  rngqiprngimfo  21208  rngqiprngfulem4  21221  znf1o  21502  freshmansdream  21525  psgnghm2  21530  elocv  21617  pjff  21663  frlmlss  21702  frlmsubgval  21716  frlmvscafval  21717  frlmvscavalb  21721  frlmvplusgscavalb  21722  frlmphl  21732  uvcresum  21744  frlmssuvc1  21745  frlmssuvc2  21746  frlmsslsp  21747  frlmup1  21749  sraassab  21818  assapropd  21822  psrelbas  21896  resspsrvsca  21939  subrgpsr  21940  psrascl  21941  mplcoe1  21997  mplbas2  22002  mplascl  22030  mplmon2cl  22034  mplmon2mul  22035  evlrhm  22064  mpfconst  22069  mhpvscacl  22101  psdascl  22115  vr1cl2  22135  ply1lss  22139  ply1subrg  22140  psropprmul  22180  ply1chr  22250  evl1vsd  22288  evl1expd  22289  evl1gsumadd  22302  evl1gsummon  22309  evls1fpws  22313  evls1vsca  22317  asclply1subcl  22318  evls1maplmhm  22321  evl1maprhm  22323  ply1vscl  22328  matring  22389  matassa  22390  mat1  22393  mattposcl  22399  mavmulass  22495  mdetunilem9  22566  matinv  22623  cpmadugsumlemF  22822  cpmadugsumfi  22823  cpmidgsum2  22825  elcls3  23031  mreclatdemoBAD  23044  neiptopnei  23080  resstps  23135  ordtrest2lem  23151  ordtrest2  23152  pnfnei  23168  mnfnei  23169  iscnp2  23187  iscnp4  23211  cnrest2r  23235  lmcls  23250  lmcld  23251  cnt0  23294  cnhaus  23302  isreg2  23325  connclo  23363  1stccnp  23410  loclly  23435  lly1stc  23444  locfincmp  23474  unisngl  23475  comppfsc  23480  kgencmp2  23494  llycmpkgen2  23498  kgen2ss  23503  kgencn3  23506  pttoponconst  23545  txcls  23552  txbasval  23554  dfac14lem  23565  ptcn  23575  ptrescn  23587  txtube  23588  txcmplem1  23589  txlm  23596  txkgen  23600  xkopjcn  23604  cnmptkp  23628  xkoinjcn  23635  qtopkgen  23658  imastps  23669  isr0  23685  r0cld  23686  pt1hmeo  23754  ptuncnv  23755  ptunhmeo  23756  filintn0  23809  trnei  23840  flimfil  23917  flimopn  23923  fbflim2  23925  cnpflf2  23948  flfcnp  23952  flfcnp2  23955  fclsopn  23962  fcfnei  23983  cnpfcf  23989  flfcntr  23991  alexsublem  23992  ptcmplem3  24002  ptcmplem4  24003  cnextfres1  24016  tmdcn2  24037  tmdgsum  24043  tmdgsum2  24044  efmndtmd  24049  symgtgp  24054  tgphaus  24065  tgpt1  24066  qustgplem  24069  prdstmdd  24072  prdstgpd  24073  haustsms  24084  tsmscls  24086  tsmsmhm  24094  tsmsadd  24095  tgptsmscls  24098  tsmssplit  24100  restutop  24186  utopreg  24201  ressusp  24213  ucncn  24234  xmetunirn  24287  ressprdsds  24321  xpsdsval  24331  xblss2ps  24351  blbas  24380  mopntopon  24389  isxms2  24398  imasf1oxms  24442  imasf1oms  24443  prdsxmslem2  24482  tmsxpsval  24491  tngngp2  24613  tngngp  24615  tgioo  24756  metdseq0  24814  cncfmpt2f  24879  cncfcnvcn  24890  cnmptre  24892  cnheibor  24925  nmhmcn  25091  cvsdiv  25103  cvsdivcl  25104  cphsubrglem  25149  cphreccllem  25150  iscmet3  25265  relcmpcmet  25290  bcthlem4  25299  rrxds  25365  rrxvsca  25366  rrxplusgvscavalb  25367  rrxbasefi  25382  rrxmetfi  25384  minveclem4  25404  mulcncf  25418  ivthicc  25431  evthicc  25432  ovolicc2lem4  25493  ovolicc2lem5  25494  iunmbl2  25530  vitalilem3  25583  cncombf  25631  cnmbf  25632  dvres2lem  25883  cpncn  25910  cpnres  25911  dvaddbr  25912  dvmulbr  25913  dvmulbrOLD  25914  dvcobr  25921  dvcobrOLD  25922  dvcjbr  25925  dvrec  25931  dvcnvlem  25952  dvlip2  25972  dvivth  25987  lhop2  25992  lhop  25993  dvcnvrelem1  25994  dvcnvrelem2  25995  dvcnvre  25996  ftc1lem6  26020  mdegvscale  26055  mdegvsca  26056  fta1blem  26150  plyaddlem1  26192  plymullem1  26193  coeeulem  26203  tayl0  26341  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulmdvlem3  26383  psercnlem2  26406  psercn  26408  efsubm  26530  cxpcn3  26728  loglesqrt  26738  efrlim  26946  efrlimOLD  26947  ppinprm  27129  chtnprm  27131  dchrptlem1  27242  dchrptlem2  27243  nodenselem5  27667  oldlim  27859  cofcutr  27890  addsproplem6  27937  negsproplem6  27991  mulsproplem13  28078  mulsproplem14  28079  noseqp1  28214  tgbtwnouttr2  28371  tgldim0eq  28379  tgifscgr  28384  iscgrglt  28390  ercgrg  28393  tgcgrxfr  28394  motcgrg  28420  tglngne  28426  tgcolg  28430  tgbtwnconn1lem2  28449  tgbtwnconn1lem3  28450  legtri3  28466  legbtwn  28470  ncolne1  28501  tgisline  28503  tglinethru  28512  coltr3  28524  colline  28525  tglowdim2ln  28527  mirinv  28542  miriso  28546  mirauto  28560  miduniq  28561  krippenlem  28566  midexlem  28568  ragperp  28593  footexALT  28594  footexlem2  28596  perpdragALT  28603  perpdrag  28604  colperpexlem1  28606  colperpexlem3  28608  mideulem2  28610  midex  28613  opphllem1  28623  opphllem3  28625  opphllem4  28626  hlpasch  28632  trgcopy  28680  f1otrg  28747  axlowdimlem16  28840  elntg  28867  eengtrkg  28869  eengtrkge  28870  clwwlkccatlem  29871  grpoidinv2  30397  grpoinv  30407  ubthlem2  30753  shuni  31182  acunirnmpt  32526  acunirnmpt2  32527  acunirnmpt2f  32528  fpwrelmap  32597  fzm1ne1  32639  fzom1ne1  32651  ccatf1  32759  swrdf1  32766  gsummpt2d  32853  gsumhashmul  32860  odpmco  32899  pmtrcnel  32902  pmtrcnel2  32903  pmtrcnelor  32904  tocyc01  32931  trsp2cyc  32936  cycpmco2f1  32937  cycpmco2rn  32938  cycpmco2lem1  32939  cycpmco2lem2  32940  cycpmco2lem3  32941  cycpmco2lem4  32942  cycpmco2lem5  32943  cycpmco2lem6  32944  cycpmco2lem7  32945  cycpmco2  32946  cycpmconjv  32955  cycpmrn  32956  tocyccntz  32957  0ringcring  33042  rloccring  33060  rloc0g  33061  rloc1r  33062  isdrng4  33083  sdrgdvcl  33085  sdrginvcl  33086  fracfld  33094  lpirlidllpi  33186  pidlnz  33188  nsgmgc  33224  rhmquskerlem  33237  elrspunidl  33240  elrspunsn  33241  drngidl  33245  qsidomlem1  33264  mxidlirred  33284  drngmxidlr  33290  opprmxidlabs  33299  opprqusplusg  33301  opprqusmulr  33303  opprqusdrng  33305  qsdrngilem  33306  qsdrngi  33307  qsdrnglem2  33308  qsdrng  33309  qsfld  33310  idlsrg0g  33318  1arithidomlem2  33348  ressdeg1  33375  ressply1invg  33378  ressply1sub  33379  ply1degltlss  33395  gsummoncoe1fzo  33396  ig1pmindeg  33400  q1pvsca  33402  r1pvsca  33403  srasubrg  33412  drgextlsp  33421  matdim  33441  lbslsat  33442  ply1degltdimlem  33448  ply1degltdim  33449  lindsunlem  33450  lbsdiflsp0  33452  dimkerim  33453  fedgmullem1  33455  fedgmullem2  33456  fedgmul  33457  fldexttr  33478  extdgmul  33481  extdg1id  33483  irngss  33493  irngnzply1lem  33496  irngnzply1  33497  irngnminplynz  33510  algextdeglem4  33516  algextdeglem8  33520  rspectopn  33596  zarclsiin  33600  zarmxt1  33609  rspectps  33612  rhmpreimacn  33614  ordtrest2NEWlem  33651  ordtrest2NEW  33652  lmxrge0  33681  nmmulg  33697  rrhcn  33726  esumadd  33804  esumaddf  33808  esumcocn  33827  measiuns  33964  mbfmco2  34013  dya2iocnrect  34029  omscl  34043  omsf  34044  oms0  34045  sibf0  34082  sibfof  34088  sitgaddlemb  34096  fibp1  34149  ccatmulgnn0dir  34302  cxpcncf1  34355  ftc2re  34358  fsum2dsub  34367  reprf  34372  reprsum  34373  bnj1450  34809  bnj1501  34826  revpfxsfxrev  34853  indispconn  34972  connpconn  34973  pconnpi1  34975  sconnpi1  34977  cvmsss2  35012  cvmliftmolem1  35019  cvmliftlem8  35030  cvmliftlem10  35032  cvmliftlem11  35033  cvmlift2lem9  35049  cvmlift2lem12  35052  cvmlift3lem7  35063  mrsubcv  35248  mrsubff  35250  mrsubccat  35256  elmrsubrn  35258  mrsubco  35259  mrsubvrs  35260  linethru  35877  ivthALT  35947  neibastop2  35973  filnetlem4  35993  matunitlindflem2  37218  poimirlem1  37222  poimirlem2  37223  poimirlem8  37229  poimirlem9  37230  poimirlem16  37237  poimirlem17  37238  poimirlem19  37240  poimirlem20  37241  poimirlem22  37243  poimirlem23  37244  poimir  37254  broucube  37255  areacirclem4  37312  fdc  37346  isbnd3  37385  prdsbnd  37394  prdstotbnd  37395  prdsbnd2  37396  rrnequiv  37436  reheibor  37440  iscringd  37599  isfldidl  37669  eqvrelth  38210  eqlkr  38698  ldualvsubval  38756  dvalveclem  40625  dia2dimlem5  40668  dia2dimlem9  40672  tendoinvcl  40704  dvhgrp  40707  dvhlveclem  40708  dihpN  40936  dochsnkr2cl  41074  lcfl7lem  41099  lclkr  41133  lclkrs  41139  lcfrvalsnN  41141  lcfrlem4  41145  lcfrlem6  41147  lcfrlem16  41158  lcdvsubval  41218  lcdlkreqN  41222  mapdcl2  41256  mapdincl  41261  mapdlsmcl  41263  mapdpglem3  41275  hdmaprnlem9N  41457  hdmaplkr  41513  hdmapip0  41515  hdmapglem7a  41527  zndvdchrrhm  41570  ressmulgnnd  41698  remexz  41704  primrootspoweq0  41706  aks6d1c1p3  41710  aks6d1c1p5  41712  aks6d1c2lem4  41727  idomnnzpownz  41732  idomnnzgmulnz  41733  ringexp0nn  41734  aks6d1c5lem0  41735  aks6d1c5lem3  41737  aks6d1c5lem2  41738  aks6d1c5  41739  sticksstones11  41756  sticksstones12a  41757  sticksstones19  41765  aks6d1c6lem2  41771  aks6d1c6lem4  41773  aks6d1c6isolem1  41774  aks6d1c6isolem2  41775  aks6d1c6lem5  41777  aks5lem2  41787  rhmpsr1  41918  evlsscaval  41929  selvvvval  41950  evlselv  41952  mhphf2  41963  mhphf4  41965  prjspnvs  42176  prjspnn0  42178  prjspner1  42182  fltnltalem  42218  diophin  42331  acongeq  42543  isnumbasgrplem2  42667  proot1mul  42761  oacl2g  42898  omabs2  42900  omcl2  42901  iunrelexpuztr  43288  ntrclsiex  43622  ntrneiiex  43645  ntrneinex  43646  elnelneqd  43771  grurankcld  43809  bccbc  43921  suctrALT  44404  restuni3  44621  disjf1o  44700  disjinfi  44701  choicefi  44709  fsneq  44715  fsneqrn  44720  unirnmapsn  44723  iunmapsn  44726  monoords  44814  elfzolem1  44838  uzfissfz  44843  monoord2xrv  45001  evthiccabs  45016  iooabslt  45019  tgqioo2  45067  islptre  45142  limciccioolb  45144  sumnnodd  45153  limcicciooub  45160  lptre2pt  45163  limcresiooub  45165  limcresioolb  45166  lptioo1cn  45169  reclimc  45176  liminfvalxr  45306  liminfvaluz  45315  limsupvaluz3  45321  fsumcncf  45401  ioccncflimc  45408  cncfuni  45409  icccncfext  45410  cncficcgt0  45411  icocncflimc  45412  cncfdmsn  45413  cncfiooicclem1  45416  cncfiooicc  45417  cncfioobd  45420  cxpcncf2  45422  fprodsub2cncf  45428  fprodadd2cncf  45429  fperdvper  45442  dvcosax  45449  dvnmul  45466  dvnprodlem1  45469  dvnprodlem2  45470  itgsubsticclem  45498  fvvolioof  45512  fvvolicof  45514  stoweidlem26  45549  stoweidlem27  45550  stoweidlem31  45554  stoweidlem34  45557  dirkercncflem2  45627  dirkercncflem3  45628  dirkercncflem4  45629  dirkercncf  45630  fourierdlem16  45646  fourierdlem20  45650  fourierdlem21  45651  fourierdlem22  45652  fourierdlem26  45656  fourierdlem32  45662  fourierdlem33  45663  fourierdlem38  45668  fourierdlem39  45669  fourierdlem46  45675  fourierdlem48  45677  fourierdlem49  45678  fourierdlem53  45682  fourierdlem60  45689  fourierdlem61  45690  fourierdlem69  45698  fourierdlem70  45699  fourierdlem71  45700  fourierdlem73  45702  fourierdlem74  45703  fourierdlem75  45704  fourierdlem76  45705  fourierdlem80  45709  fourierdlem81  45710  fourierdlem82  45711  fourierdlem83  45712  fourierdlem84  45713  fourierdlem85  45714  fourierdlem88  45717  fourierdlem89  45718  fourierdlem91  45720  fourierdlem92  45721  fourierdlem93  45722  fourierdlem100  45729  fourierdlem101  45730  fourierdlem103  45732  fourierdlem104  45733  fourierdlem107  45736  fourierdlem111  45740  fourierdlem112  45741  fourierdlem113  45742  fouriersw  45754  fouriercn  45755  etransclem24  45781  etransclem26  45783  etransclem28  45785  etransclem31  45788  etransclem32  45789  etransclem33  45790  etransclem34  45791  etransclem35  45792  etransclem38  45795  rrxtopnfi  45810  rrxtoponfi  45814  qndenserrnbl  45818  qndenserrnopnlem  45820  qndenserrn  45822  rrnprjdstle  45824  ioorrnopnlem  45827  prsal  45841  intsaluni  45852  salgencntex  45866  subsaliuncllem  45880  fge0iccico  45893  sge0sn  45902  sge0tsms  45903  sge0cl  45904  sge0f1o  45905  sge0pr  45917  sge0isum  45950  nnfoctbdjlem  45978  iundjiunlem  45982  iundjiun  45983  meadjiunlem  45988  psmeasure  45994  meaiininclem  46009  caragenelss  46024  omeunile  46028  carageniuncllem1  46044  carageniuncllem2  46045  0ome  46052  isomenndlem  46053  isomennd  46054  hoicvr  46071  ovnpnfelsup  46082  ovncvrrp  46087  ovnsubaddlem1  46093  hoidmv1le  46117  hoidmvlelem2  46119  hoidmvlelem3  46120  hoidmvlelem4  46121  hoidmvle  46123  ovnhoilem1  46124  hoi2toco  46130  ovncvr2  46134  hspdifhsp  46139  voncmpl  46144  hoiqssbl  46148  hspmbllem2  46150  hspmbl  46152  hoimbllem  46153  opnvonmbllem2  46156  mblvon  46162  ovolval3  46170  ovolval4lem1  46172  ovnovollem1  46179  ovnovollem2  46180  vonsn  46214  issmflem  46250  sssmf  46261  issmflelem  46267  issmfgtlem  46278  issmfgt  46279  smfaddlem1  46286  issmfgelem  46292  smflimlem3  46296  smfmullem2  46315  smfmullem4  46317  smfsuplem1  46334  smfsupmpt  46338  smfinfmpt  46342  smflimsuplem2  46344  smflimsuplem4  46346  smflimsupmpt  46352  smfliminfmpt  46355  fsupdm  46365  finfdm  46369  zlmodzxzel  47602  ply1mulgsum  47641  catprs  48200  thincmod  48220  mndtcob  48277  mndtccatid  48282  mndtcid  48284  grptcmon  48285  grptcepi  48286