Theorem eleqtrd 2836

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eleqtrrd  2837  eleqtrid  2840  eleqtrdi  2844  3eltr3d  2848  prel12g  4864  opth1  5475  0nelop  5496  fvelimad  6957  fviss  6966  tfisi  7845  fnwelem  8114  frrlem8  8275  frrlem10  8277  fprresex  8292  wfrlem17OLD  8322  omeulem1  8579  oeeulem  8598  oeeui  8599  oaabs2  8645  omabs  8647  ercl  8711  erth  8749  ecelqsdm  8778  ordtypelem6  9515  ordtypelem7  9516  cantnfval  9660  cantnfp1lem3  9672  cantnflem4  9684  r1pwss  9776  rankonidlem  9820  rankxplim3  9873  fseqenlem2  10017  iunfictbso  10106  dfac12lem1  10135  dfac12lem2  10136  fin23lem30  10334  iundom2g  10532  fpwwe2lem5  10627  fpwwe2lem8  10630  lincmb01cmp  13469  fzopth  13535  fzoaddel2  13685  fzosubel2  13689  fzocatel  13693  zpnn0elfzo1  13703  fzoend  13720  peano2fzor  13736  monoord2  13996  sermono  13997  expmulnbnd  14195  bcpasc  14278  hash1elsn  14328  swrdcl  14592  revcl  14708  revlen  14709  fsum0diag2  15726  isumsplit  15783  fprodser  15890  sadadd  16405  sadass  16409  smuval2  16420  smumul  16431  vdwapun  16904  vdwlem9  16919  ramub1lem1  16956  prdsbasfn  17414  prdsbasprj  17415  pwsplusgval  17433  pwsmulrval  17434  pwsvscafval  17437  xpsaddlem  17516  xpsvsca  17520  xpsle  17522  mreexmrid  17584  homfeqval  17638  comfval2  17644  comfeq  17647  comfeqval  17649  oppccomfpropd  17670  invco  17715  sectepi  17728  issubc3  17796  funcf2  17815  fthepi  17876  nat1st2nd  17899  homarcl2  17982  coapm  18018  setcmon  18034  setcepi  18035  setcsect  18036  setcinv  18037  setciso  18038  cat1lem  18043  catccatid  18053  resscatc  18056  catciso  18058  catcbascl  18059  catcoppccl  18064  catcoppcclOLD  18065  catcfuccl  18066  catcfucclOLD  18067  xpccatid  18137  catcxpccl  18156  catcxpcclOLD  18157  xpcpropd  18158  evlfcl  18172  curfpropd  18183  hofcl  18209  yonedalem3  18230  yonffthlem  18232  poslubdg  18364  grpidd  18587  gsumress  18598  sgrppropd  18619  ismndd  18644  mndpropd  18647  issubmnd  18649  submnd0  18651  imasmnd  18660  xpsmnd0  18663  frmdelbas  18731  grpidd2  18859  pwsinvg  18933  imasgrp  18936  submmulg  18993  subginvcl  19010  subgcl  19011  subgsub  19013  subgmulg  19015  1nsgtrivd  19049  quseccl0  19059  gaid2  19162  finodsubmsubg  19430  submod  19432  odsubdvds  19434  sylow1lem4  19464  sylow2alem2  19481  lsmdisj2  19545  subgdisj1  19554  pj1id  19562  efgsrel  19597  efgrelexlemb  19613  efgcpbl2  19620  frgpcpbl  19622  frgp0  19623  frgpeccl  19624  frgpadd  19626  frgpup3lem  19640  frgpnabllem1  19736  cycsubgcyg  19764  prdsgsum  19844  dprdfeq0  19887  dmdprdsplitlem  19902  dpjidcl  19923  pgpfac1lem3a  19941  pgpfac1lem4  19943  pgpfaclem1  19946  pgpfaclem2  19947  ablfaclem2  19951  simpgnsgeqd  19966  simpgnsgbid  19968  ablsimpnosubgd  19969  ringidss  20088  ringpropd  20096  imasring  20137  qusring2  20140  kerf1ghm  20275  lringuplu  20307  subrg1  20366  subrgmcl  20368  subrgdv  20373  subrgunit  20374  issubdrg  20382  resrhm  20386  lmodprop2d  20527  0lmhm  20644  lmhmpropd  20677  lspfixed  20734  lssacsex  20750  lbsextlem4  20767  quscrng  20871  znf1o  21099  psgnghm2  21126  elocv  21213  pjff  21259  frlmlss  21298  frlmsubgval  21312  frlmvscafval  21313  frlmvscavalb  21317  frlmvplusgscavalb  21318  frlmphl  21328  uvcresum  21340  frlmssuvc1  21341  frlmssuvc2  21342  frlmsslsp  21343  frlmup1  21345  sraassab  21414  assapropd  21418  psrelbas  21490  resspsrvsca  21530  subrgpsr  21531  mplcoe1  21584  mplbas2  21589  mplascl  21617  mplmon2cl  21621  mplmon2mul  21622  evlrhm  21651  mpfconst  21656  mhpvscacl  21689  vr1cl2  21709  ply1lss  21712  ply1subrg  21713  psropprmul  21752  evl1vsd  21855  evl1expd  21856  evl1gsumadd  21869  evl1gsummon  21876  matring  21937  matassa  21938  mat1  21941  mattposcl  21947  mavmulass  22043  mdetunilem9  22114  matinv  22171  cpmadugsumlemF  22370  cpmadugsumfi  22371  cpmidgsum2  22373  elcls3  22579  mreclatdemoBAD  22592  neiptopnei  22628  resstps  22683  ordtrest2lem  22699  ordtrest2  22700  pnfnei  22716  mnfnei  22717  iscnp2  22735  iscnp4  22759  cnrest2r  22783  lmcls  22798  lmcld  22799  cnt0  22842  cnhaus  22850  isreg2  22873  connclo  22911  1stccnp  22958  loclly  22983  lly1stc  22992  locfincmp  23022  unisngl  23023  comppfsc  23028  kgencmp2  23042  llycmpkgen2  23046  kgen2ss  23051  kgencn3  23054  pttoponconst  23093  txcls  23100  txbasval  23102  dfac14lem  23113  ptcn  23123  ptrescn  23135  txtube  23136  txcmplem1  23137  txlm  23144  txkgen  23148  xkopjcn  23152  cnmptkp  23176  xkoinjcn  23183  qtopkgen  23206  imastps  23217  isr0  23233  r0cld  23234  pt1hmeo  23302  ptuncnv  23303  ptunhmeo  23304  filintn0  23357  trnei  23388  flimfil  23465  flimopn  23471  fbflim2  23473  cnpflf2  23496  flfcnp  23500  flfcnp2  23503  fclsopn  23510  fcfnei  23531  cnpfcf  23537  flfcntr  23539  alexsublem  23540  ptcmplem3  23550  ptcmplem4  23551  cnextfres1  23564  tmdcn2  23585  tmdgsum  23591  tmdgsum2  23592  efmndtmd  23597  symgtgp  23602  tgphaus  23613  tgpt1  23614  qustgplem  23617  prdstmdd  23620  prdstgpd  23621  haustsms  23632  tsmscls  23634  tsmsmhm  23642  tsmsadd  23643  tgptsmscls  23646  tsmssplit  23648  restutop  23734  utopreg  23749  ressusp  23761  ucncn  23782  xmetunirn  23835  ressprdsds  23869  xpsdsval  23879  xblss2ps  23899  blbas  23928  mopntopon  23937  isxms2  23946  imasf1oxms  23990  imasf1oms  23991  prdsxmslem2  24030  tmsxpsval  24039  tngngp2  24161  tngngp  24163  tgioo  24304  metdseq0  24362  cncfmpt2f  24423  cncfcnvcn  24433  cnmptre  24435  cnheibor  24463  nmhmcn  24628  cvsdiv  24640  cvsdivcl  24641  cphsubrglem  24686  cphreccllem  24687  iscmet3  24802  relcmpcmet  24827  bcthlem4  24836  rrxds  24902  rrxvsca  24903  rrxplusgvscavalb  24904  rrxbasefi  24919  rrxmetfi  24921  minveclem4  24941  ivthicc  24967  evthicc  24968  ovolicc2lem4  25029  ovolicc2lem5  25030  iunmbl2  25066  vitalilem3  25119  cncombf  25167  cnmbf  25168  dvres2lem  25419  cpncn  25445  cpnres  25446  dvaddbr  25447  dvmulbr  25448  dvcobr  25455  dvcjbr  25458  dvrec  25464  dvcnvlem  25485  dvlip2  25504  dvivth  25519  lhop2  25524  lhop  25525  dvcnvrelem1  25526  dvcnvrelem2  25527  dvcnvre  25528  ftc1lem6  25550  mdegvscale  25585  mdegvsca  25586  fta1blem  25678  plyaddlem1  25719  plymullem1  25720  coeeulem  25730  tayl0  25866  taylthlem1  25877  taylthlem2  25878  ulmdvlem3  25906  psercnlem2  25928  psercn  25930  efsubm  26052  cxpcn3  26246  loglesqrt  26256  efrlim  26464  ppinprm  26646  chtnprm  26648  dchrptlem1  26757  dchrptlem2  26758  nodenselem5  27181  oldlim  27371  cofcutr  27401  addsproplem6  27448  negsproplem6  27497  mulsproplem13  27574  mulsproplem14  27575  tgbtwnouttr2  27736  tgldim0eq  27744  tgifscgr  27749  iscgrglt  27755  ercgrg  27758  tgcgrxfr  27759  motcgrg  27785  tglngne  27791  tgcolg  27795  tgbtwnconn1lem2  27814  tgbtwnconn1lem3  27815  legtri3  27831  legbtwn  27835  ncolne1  27866  tgisline  27868  tglinethru  27877  coltr3  27889  colline  27890  tglowdim2ln  27892  mirinv  27907  miriso  27911  mirauto  27925  miduniq  27926  krippenlem  27931  midexlem  27933  ragperp  27958  footexALT  27959  footexlem2  27961  perpdragALT  27968  perpdrag  27969  colperpexlem1  27971  colperpexlem3  27973  mideulem2  27975  midex  27978  opphllem1  27988  opphllem3  27990  opphllem4  27991  hlpasch  27997  trgcopy  28045  f1otrg  28112  axlowdimlem16  28205  elntg  28232  eengtrkg  28234  eengtrkge  28235  clwwlkccatlem  29232  grpoidinv2  29756  grpoinv  29766  ubthlem2  30112  shuni  30541  acunirnmpt  31872  acunirnmpt2  31873  acunirnmpt2f  31874  fpwrelmap  31946  fzm1ne1  31988  fzom1ne1  32000  ccatf1  32103  swrdf1  32108  gsummpt2d  32189  gsumhashmul  32196  odpmco  32235  pmtrcnel  32238  pmtrcnel2  32239  pmtrcnelor  32240  tocyc01  32265  trsp2cyc  32270  cycpmco2f1  32271  cycpmco2rn  32272  cycpmco2lem1  32273  cycpmco2lem2  32274  cycpmco2lem3  32275  cycpmco2lem4  32276  cycpmco2lem5  32277  cycpmco2lem6  32278  cycpmco2lem7  32279  cycpmco2  32280  cycpmconjv  32289  cycpmrn  32290  tocyccntz  32291  rngurd  32368  freshmansdream  32370  isdrng4  32384  sdrgdvcl  32386  sdrginvcl  32387  pidlnz  32477  qusmul  32504  nsgmgc  32512  ghmquskerlem1  32517  ghmquskerco  32518  ghmqusker  32521  rhmquskerlem  32532  elrspunidl  32535  elrspunsn  32536  drngidl  32540  qsidomlem1  32560  mxidlirred  32577  opprmxidlabs  32590  opprqusplusg  32592  opprqusmulr  32594  opprqusdrng  32596  qsdrngilem  32597  qsdrngi  32598  qsdrnglem2  32599  qsdrng  32600  qsfld  32601  idlsrg0g  32609  evls1fpws  32635  evls1vsca  32639  ressdeg1  32640  ressply1invg  32647  ressply1sub  32648  asclply1subcl  32649  ply1chr  32650  ply1degltlss  32656  gsummoncoe1fzo  32657  ig1pmindeg  32660  srasubrg  32663  drgextlsp  32670  matdim  32689  lbslsat  32690  ply1degltdimlem  32696  ply1degltdim  32697  lindsunlem  32698  lbsdiflsp0  32700  dimkerim  32701  fedgmullem1  32703  fedgmullem2  32704  fedgmul  32705  fldexttr  32726  extdgmul  32729  extdg1id  32731  irngss  32740  irngnzply1lem  32743  irngnzply1  32744  evls1maplmhm  32749  irngnminplynz  32760  algextdeglem1  32761  rspectopn  32836  zarclsiin  32840  zarmxt1  32849  rspectps  32852  rhmpreimacn  32854  ordtrest2NEWlem  32891  ordtrest2NEW  32892  lmxrge0  32921  nmmulg  32937  rrhcn  32966  esumadd  33044  esumaddf  33048  esumcocn  33067  measiuns  33204  mbfmco2  33253  dya2iocnrect  33269  omscl  33283  omsf  33284  oms0  33285  sibf0  33322  sibfof  33328  sitgaddlemb  33336  fibp1  33389  ccatmulgnn0dir  33542  cxpcncf1  33596  ftc2re  33599  fsum2dsub  33608  reprf  33613  reprsum  33614  bnj1450  34050  bnj1501  34067  revpfxsfxrev  34095  indispconn  34214  connpconn  34215  pconnpi1  34217  sconnpi1  34219  cvmsss2  34254  cvmliftmolem1  34261  cvmliftlem8  34272  cvmliftlem10  34274  cvmliftlem11  34275  cvmlift2lem9  34291  cvmlift2lem12  34294  cvmlift3lem7  34305  mrsubcv  34490  mrsubff  34492  mrsubccat  34498  elmrsubrn  34500  mrsubco  34501  mrsubvrs  34502  linethru  35114  gg-mulcncf  35162  gg-dvmulbr  35164  gg-dvcobr  35165  ivthALT  35209  neibastop2  35235  filnetlem4  35255  matunitlindflem2  36474  poimirlem1  36478  poimirlem2  36479  poimirlem8  36485  poimirlem9  36486  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem22  36499  poimirlem23  36500  poimir  36510  broucube  36511  areacirclem4  36568  fdc  36602  isbnd3  36641  prdsbnd  36650  prdstotbnd  36651  prdsbnd2  36652  rrnequiv  36692  reheibor  36696  iscringd  36855  isfldidl  36925  eqvrelth  37470  eqlkr  37958  ldualvsubval  38016  dvalveclem  39885  dia2dimlem5  39928  dia2dimlem9  39932  tendoinvcl  39964  dvhgrp  39967  dvhlveclem  39968  dihpN  40196  dochsnkr2cl  40334  lcfl7lem  40359  lclkr  40393  lclkrs  40399  lcfrvalsnN  40401  lcfrlem4  40405  lcfrlem6  40407  lcfrlem16  40418  lcdvsubval  40478  lcdlkreqN  40482  mapdcl2  40516  mapdincl  40521  mapdlsmcl  40523  mapdpglem3  40535  hdmaprnlem9N  40717  hdmaplkr  40773  hdmapip0  40775  hdmapglem7a  40787  sticksstones11  40961  sticksstones12a  40962  sticksstones19  40970  evlsscaval  41134  selvvvval  41155  evlselv  41157  mhphf2  41168  mhphf4  41170  prjspnvs  41359  prjspnn0  41361  prjspner1  41365  fltnltalem  41401  diophin  41496  acongeq  41708  isnumbasgrplem2  41832  proot1mul  41927  oacl2g  42066  omabs2  42068  omcl2  42069  iunrelexpuztr  42456  ntrclsiex  42790  ntrneiiex  42813  ntrneinex  42814  elnelneqd  42940  grurankcld  42978  bccbc  43090  suctrALT  43573  restuni3  43793  disjf1o  43875  disjinfi  43877  choicefi  43885  fsneq  43891  fsneqrn  43896  unirnmapsn  43899  iunmapsn  43902  monoords  43994  elfzolem1  44018  uzfissfz  44023  monoord2xrv  44181  evthiccabs  44196  iooabslt  44199  tgqioo2  44247  islptre  44322  limciccioolb  44324  sumnnodd  44333  limcicciooub  44340  lptre2pt  44343  limcresiooub  44345  limcresioolb  44346  lptioo1cn  44349  reclimc  44356  liminfvalxr  44486  liminfvaluz  44495  limsupvaluz3  44501  fsumcncf  44581  ioccncflimc  44588  cncfuni  44589  icccncfext  44590  cncficcgt0  44591  icocncflimc  44592  cncfdmsn  44593  cncfiooicclem1  44596  cncfiooicc  44597  cncfioobd  44600  cxpcncf2  44602  fprodsub2cncf  44608  fprodadd2cncf  44609  fperdvper  44622  dvcosax  44629  dvnmul  44646  dvnprodlem1  44649  dvnprodlem2  44650  itgsubsticclem  44678  fvvolioof  44692  fvvolicof  44694  stoweidlem26  44729  stoweidlem27  44730  stoweidlem31  44734  stoweidlem34  44737  dirkercncflem2  44807  dirkercncflem3  44808  dirkercncflem4  44809  dirkercncf  44810  fourierdlem16  44826  fourierdlem20  44830  fourierdlem21  44831  fourierdlem22  44832  fourierdlem26  44836  fourierdlem32  44842  fourierdlem33  44843  fourierdlem38  44848  fourierdlem39  44849  fourierdlem46  44855  fourierdlem48  44857  fourierdlem49  44858  fourierdlem53  44862  fourierdlem60  44869  fourierdlem61  44870  fourierdlem69  44878  fourierdlem70  44879  fourierdlem71  44880  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem80  44889  fourierdlem81  44890  fourierdlem82  44891  fourierdlem83  44892  fourierdlem84  44893  fourierdlem85  44894  fourierdlem88  44897  fourierdlem89  44898  fourierdlem91  44900  fourierdlem92  44901  fourierdlem93  44902  fourierdlem100  44909  fourierdlem101  44910  fourierdlem103  44912  fourierdlem104  44913  fourierdlem107  44916  fourierdlem111  44920  fourierdlem112  44921  fourierdlem113  44922  fouriersw  44934  fouriercn  44935  etransclem24  44961  etransclem26  44963  etransclem28  44965  etransclem31  44968  etransclem32  44969  etransclem33  44970  etransclem34  44971  etransclem35  44972  etransclem38  44975  rrxtopnfi  44990  rrxtoponfi  44994  qndenserrnbl  44998  qndenserrnopnlem  45000  qndenserrn  45002  rrnprjdstle  45004  ioorrnopnlem  45007  prsal  45021  intsaluni  45032  salgencntex  45046  subsaliuncllem  45060  fge0iccico  45073  sge0sn  45082  sge0tsms  45083  sge0cl  45084  sge0f1o  45085  sge0pr  45097  sge0isum  45130  nnfoctbdjlem  45158  iundjiunlem  45162  iundjiun  45163  meadjiunlem  45168  psmeasure  45174  meaiininclem  45189  caragenelss  45204  omeunile  45208  carageniuncllem1  45224  carageniuncllem2  45225  0ome  45232  isomenndlem  45233  isomennd  45234  hoicvr  45251  ovnpnfelsup  45262  ovncvrrp  45267  ovnsubaddlem1  45273  hoidmv1le  45297  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  hoidmvle  45303  ovnhoilem1  45304  hoi2toco  45310  ovncvr2  45314  hspdifhsp  45319  voncmpl  45324  hoiqssbl  45328  hspmbllem2  45330  hspmbl  45332  hoimbllem  45333  opnvonmbllem2  45336  mblvon  45342  ovolval3  45350  ovolval4lem1  45352  ovnovollem1  45359  ovnovollem2  45360  vonsn  45394  issmflem  45430  sssmf  45441  issmflelem  45447  issmfgtlem  45458  issmfgt  45459  smfaddlem1  45466  issmfgelem  45472  smflimlem3  45476  smfmullem2  45495  smfmullem4  45497  smfsuplem1  45514  smfsupmpt  45518  smfinfmpt  45522  smflimsuplem2  45524  smflimsuplem4  45526  smflimsupmpt  45532  smfliminfmpt  45535  fsupdm  45545  finfdm  45549  fzoopth  46022  issubmgm2  46547  rngpropd  46660  imasrng  46665  subrngmcl  46721  rngqiprnglinlem1  46757  rngqiprngimf  46763  rngqiprngimfo  46767  zlmodzxzel  46985  ply1mulgsum  47025  catprs  47585  thincmod  47605  mndtcob  47662  mndtccatid  47667  mndtcid  47669  grptcmon  47670  grptcepi  47671