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  4865  opth1  5476  0nelop  5497  fvelimad  6960  fviss  6969  tfisi  7848  fnwelem  8117  frrlem8  8278  frrlem10  8280  fprresex  8295  wfrlem17OLD  8325  omeulem1  8582  oeeulem  8601  oeeui  8602  oaabs2  8648  omabs  8650  ercl  8714  erth  8752  ecelqsdm  8781  ordtypelem6  9518  ordtypelem7  9519  cantnfval  9663  cantnfp1lem3  9675  cantnflem4  9687  r1pwss  9779  rankonidlem  9823  rankxplim3  9876  fseqenlem2  10020  iunfictbso  10109  dfac12lem1  10138  dfac12lem2  10139  fin23lem30  10337  iundom2g  10535  fpwwe2lem5  10630  fpwwe2lem8  10633  lincmb01cmp  13472  fzopth  13538  fzoaddel2  13688  fzosubel2  13692  fzocatel  13696  zpnn0elfzo1  13706  fzoend  13723  peano2fzor  13739  monoord2  13999  sermono  14000  expmulnbnd  14198  bcpasc  14281  hash1elsn  14331  swrdcl  14595  revcl  14711  revlen  14712  fsum0diag2  15729  isumsplit  15786  fprodser  15893  sadadd  16408  sadass  16412  smuval2  16423  smumul  16434  vdwapun  16907  vdwlem9  16922  ramub1lem1  16959  prdsbasfn  17417  prdsbasprj  17418  pwsplusgval  17436  pwsmulrval  17437  pwsvscafval  17440  xpsaddlem  17519  xpsvsca  17523  xpsle  17525  mreexmrid  17587  homfeqval  17641  comfval2  17647  comfeq  17650  comfeqval  17652  oppccomfpropd  17673  invco  17718  sectepi  17731  issubc3  17799  funcf2  17818  fthepi  17879  nat1st2nd  17902  homarcl2  17985  coapm  18021  setcmon  18037  setcepi  18038  setcsect  18039  setcinv  18040  setciso  18041  cat1lem  18046  catccatid  18056  resscatc  18059  catciso  18061  catcbascl  18062  catcoppccl  18067  catcoppcclOLD  18068  catcfuccl  18069  catcfucclOLD  18070  xpccatid  18140  catcxpccl  18159  catcxpcclOLD  18160  xpcpropd  18161  evlfcl  18175  curfpropd  18186  hofcl  18212  yonedalem3  18233  yonffthlem  18235  poslubdg  18367  grpidd  18590  gsumress  18601  sgrppropd  18622  ismndd  18647  mndpropd  18650  issubmnd  18652  submnd0  18654  imasmnd  18663  xpsmnd0  18666  frmdelbas  18734  grpidd2  18862  pwsinvg  18936  imasgrp  18939  xpsinv  18943  xpsgrpsub  18944  submmulg  18998  subginvcl  19015  subgcl  19016  subgsub  19018  subgmulg  19020  1nsgtrivd  19054  quseccl0  19064  gaid2  19167  finodsubmsubg  19435  submod  19437  odsubdvds  19439  sylow1lem4  19469  sylow2alem2  19486  lsmdisj2  19550  subgdisj1  19559  pj1id  19567  efgsrel  19602  efgrelexlemb  19618  efgcpbl2  19625  frgpcpbl  19627  frgp0  19628  frgpeccl  19629  frgpadd  19631  frgpup3lem  19645  frgpnabllem1  19741  cycsubgcyg  19769  prdsgsum  19849  dprdfeq0  19892  dmdprdsplitlem  19907  dpjidcl  19928  pgpfac1lem3a  19946  pgpfac1lem4  19948  pgpfaclem1  19951  pgpfaclem2  19952  ablfaclem2  19956  simpgnsgeqd  19971  simpgnsgbid  19973  ablsimpnosubgd  19974  ringurd  20008  ringidss  20094  ringpropd  20102  imasring  20143  xpsring1d  20146  qusring2  20147  kerf1ghm  20282  lringuplu  20314  subrg1  20329  subrgmcl  20331  subrgdv  20336  subrgunit  20337  resrhm  20348  issubdrg  20401  lmodprop2d  20534  0lmhm  20651  lmhmpropd  20684  lspfixed  20741  lssacsex  20757  lbsextlem4  20774  quscrng  20878  znf1o  21107  psgnghm2  21134  elocv  21221  pjff  21267  frlmlss  21306  frlmsubgval  21320  frlmvscafval  21321  frlmvscavalb  21325  frlmvplusgscavalb  21326  frlmphl  21336  uvcresum  21348  frlmssuvc1  21349  frlmssuvc2  21350  frlmsslsp  21351  frlmup1  21353  sraassab  21422  assapropd  21426  psrelbas  21498  resspsrvsca  21538  subrgpsr  21539  mplcoe1  21592  mplbas2  21597  mplascl  21625  mplmon2cl  21629  mplmon2mul  21630  evlrhm  21659  mpfconst  21664  mhpvscacl  21697  vr1cl2  21717  ply1lss  21720  ply1subrg  21721  psropprmul  21760  evl1vsd  21863  evl1expd  21864  evl1gsumadd  21877  evl1gsummon  21884  matring  21945  matassa  21946  mat1  21949  mattposcl  21955  mavmulass  22051  mdetunilem9  22122  matinv  22179  cpmadugsumlemF  22378  cpmadugsumfi  22379  cpmidgsum2  22381  elcls3  22587  mreclatdemoBAD  22600  neiptopnei  22636  resstps  22691  ordtrest2lem  22707  ordtrest2  22708  pnfnei  22724  mnfnei  22725  iscnp2  22743  iscnp4  22767  cnrest2r  22791  lmcls  22806  lmcld  22807  cnt0  22850  cnhaus  22858  isreg2  22881  connclo  22919  1stccnp  22966  loclly  22991  lly1stc  23000  locfincmp  23030  unisngl  23031  comppfsc  23036  kgencmp2  23050  llycmpkgen2  23054  kgen2ss  23059  kgencn3  23062  pttoponconst  23101  txcls  23108  txbasval  23110  dfac14lem  23121  ptcn  23131  ptrescn  23143  txtube  23144  txcmplem1  23145  txlm  23152  txkgen  23156  xkopjcn  23160  cnmptkp  23184  xkoinjcn  23191  qtopkgen  23214  imastps  23225  isr0  23241  r0cld  23242  pt1hmeo  23310  ptuncnv  23311  ptunhmeo  23312  filintn0  23365  trnei  23396  flimfil  23473  flimopn  23479  fbflim2  23481  cnpflf2  23504  flfcnp  23508  flfcnp2  23511  fclsopn  23518  fcfnei  23539  cnpfcf  23545  flfcntr  23547  alexsublem  23548  ptcmplem3  23558  ptcmplem4  23559  cnextfres1  23572  tmdcn2  23593  tmdgsum  23599  tmdgsum2  23600  efmndtmd  23605  symgtgp  23610  tgphaus  23621  tgpt1  23622  qustgplem  23625  prdstmdd  23628  prdstgpd  23629  haustsms  23640  tsmscls  23642  tsmsmhm  23650  tsmsadd  23651  tgptsmscls  23654  tsmssplit  23656  restutop  23742  utopreg  23757  ressusp  23769  ucncn  23790  xmetunirn  23843  ressprdsds  23877  xpsdsval  23887  xblss2ps  23907  blbas  23936  mopntopon  23945  isxms2  23954  imasf1oxms  23998  imasf1oms  23999  prdsxmslem2  24038  tmsxpsval  24047  tngngp2  24169  tngngp  24171  tgioo  24312  metdseq0  24370  cncfmpt2f  24431  cncfcnvcn  24441  cnmptre  24443  cnheibor  24471  nmhmcn  24636  cvsdiv  24648  cvsdivcl  24649  cphsubrglem  24694  cphreccllem  24695  iscmet3  24810  relcmpcmet  24835  bcthlem4  24844  rrxds  24910  rrxvsca  24911  rrxplusgvscavalb  24912  rrxbasefi  24927  rrxmetfi  24929  minveclem4  24949  ivthicc  24975  evthicc  24976  ovolicc2lem4  25037  ovolicc2lem5  25038  iunmbl2  25074  vitalilem3  25127  cncombf  25175  cnmbf  25176  dvres2lem  25427  cpncn  25453  cpnres  25454  dvaddbr  25455  dvmulbr  25456  dvcobr  25463  dvcjbr  25466  dvrec  25472  dvcnvlem  25493  dvlip2  25512  dvivth  25527  lhop2  25532  lhop  25533  dvcnvrelem1  25534  dvcnvrelem2  25535  dvcnvre  25536  ftc1lem6  25558  mdegvscale  25593  mdegvsca  25594  fta1blem  25686  plyaddlem1  25727  plymullem1  25728  coeeulem  25738  tayl0  25874  taylthlem1  25885  taylthlem2  25886  ulmdvlem3  25914  psercnlem2  25936  psercn  25938  efsubm  26060  cxpcn3  26256  loglesqrt  26266  efrlim  26474  ppinprm  26656  chtnprm  26658  dchrptlem1  26767  dchrptlem2  26768  nodenselem5  27191  oldlim  27381  cofcutr  27411  addsproplem6  27458  negsproplem6  27507  mulsproplem13  27584  mulsproplem14  27585  tgbtwnouttr2  27746  tgldim0eq  27754  tgifscgr  27759  iscgrglt  27765  ercgrg  27768  tgcgrxfr  27769  motcgrg  27795  tglngne  27801  tgcolg  27805  tgbtwnconn1lem2  27824  tgbtwnconn1lem3  27825  legtri3  27841  legbtwn  27845  ncolne1  27876  tgisline  27878  tglinethru  27887  coltr3  27899  colline  27900  tglowdim2ln  27902  mirinv  27917  miriso  27921  mirauto  27935  miduniq  27936  krippenlem  27941  midexlem  27943  ragperp  27968  footexALT  27969  footexlem2  27971  perpdragALT  27978  perpdrag  27979  colperpexlem1  27981  colperpexlem3  27983  mideulem2  27985  midex  27988  opphllem1  27998  opphllem3  28000  opphllem4  28001  hlpasch  28007  trgcopy  28055  f1otrg  28122  axlowdimlem16  28215  elntg  28242  eengtrkg  28244  eengtrkge  28245  clwwlkccatlem  29242  grpoidinv2  29768  grpoinv  29778  ubthlem2  30124  shuni  30553  acunirnmpt  31884  acunirnmpt2  31885  acunirnmpt2f  31886  fpwrelmap  31958  fzm1ne1  32000  fzom1ne1  32012  ccatf1  32115  swrdf1  32120  gsummpt2d  32201  gsumhashmul  32208  odpmco  32247  pmtrcnel  32250  pmtrcnel2  32251  pmtrcnelor  32252  tocyc01  32277  trsp2cyc  32282  cycpmco2f1  32283  cycpmco2rn  32284  cycpmco2lem1  32285  cycpmco2lem2  32286  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmco2  32292  cycpmconjv  32301  cycpmrn  32302  tocyccntz  32303  freshmansdream  32381  isdrng4  32395  sdrgdvcl  32397  sdrginvcl  32398  pidlnz  32488  qusmul  32515  nsgmgc  32523  ghmquskerlem1  32528  ghmquskerco  32529  ghmqusker  32532  rhmquskerlem  32543  elrspunidl  32546  elrspunsn  32547  drngidl  32551  qsidomlem1  32571  mxidlirred  32588  opprmxidlabs  32601  opprqusplusg  32603  opprqusmulr  32605  opprqusdrng  32607  qsdrngilem  32608  qsdrngi  32609  qsdrnglem2  32610  qsdrng  32611  qsfld  32612  idlsrg0g  32620  evls1fpws  32646  evls1vsca  32650  ressdeg1  32651  ressply1invg  32658  ressply1sub  32659  asclply1subcl  32660  ply1chr  32661  ply1degltlss  32667  gsummoncoe1fzo  32668  ig1pmindeg  32671  srasubrg  32674  drgextlsp  32681  matdim  32700  lbslsat  32701  ply1degltdimlem  32707  ply1degltdim  32708  lindsunlem  32709  lbsdiflsp0  32711  dimkerim  32712  fedgmullem1  32714  fedgmullem2  32715  fedgmul  32716  fldexttr  32737  extdgmul  32740  extdg1id  32742  irngss  32751  irngnzply1lem  32754  irngnzply1  32755  evls1maplmhm  32760  irngnminplynz  32771  algextdeglem1  32772  rspectopn  32847  zarclsiin  32851  zarmxt1  32860  rspectps  32863  rhmpreimacn  32865  ordtrest2NEWlem  32902  ordtrest2NEW  32903  lmxrge0  32932  nmmulg  32948  rrhcn  32977  esumadd  33055  esumaddf  33059  esumcocn  33078  measiuns  33215  mbfmco2  33264  dya2iocnrect  33280  omscl  33294  omsf  33295  oms0  33296  sibf0  33333  sibfof  33339  sitgaddlemb  33347  fibp1  33400  ccatmulgnn0dir  33553  cxpcncf1  33607  ftc2re  33610  fsum2dsub  33619  reprf  33624  reprsum  33625  bnj1450  34061  bnj1501  34078  revpfxsfxrev  34106  indispconn  34225  connpconn  34226  pconnpi1  34228  sconnpi1  34230  cvmsss2  34265  cvmliftmolem1  34272  cvmliftlem8  34283  cvmliftlem10  34285  cvmliftlem11  34286  cvmlift2lem9  34302  cvmlift2lem12  34305  cvmlift3lem7  34316  mrsubcv  34501  mrsubff  34503  mrsubccat  34509  elmrsubrn  34511  mrsubco  34512  mrsubvrs  34513  linethru  35125  gg-mulcncf  35173  gg-dvmulbr  35175  gg-dvcobr  35176  ivthALT  35220  neibastop2  35246  filnetlem4  35266  matunitlindflem2  36485  poimirlem1  36489  poimirlem2  36490  poimirlem8  36496  poimirlem9  36497  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimir  36521  broucube  36522  areacirclem4  36579  fdc  36613  isbnd3  36652  prdsbnd  36661  prdstotbnd  36662  prdsbnd2  36663  rrnequiv  36703  reheibor  36707  iscringd  36866  isfldidl  36936  eqvrelth  37481  eqlkr  37969  ldualvsubval  38027  dvalveclem  39896  dia2dimlem5  39939  dia2dimlem9  39943  tendoinvcl  39975  dvhgrp  39978  dvhlveclem  39979  dihpN  40207  dochsnkr2cl  40345  lcfl7lem  40370  lclkr  40404  lclkrs  40410  lcfrvalsnN  40412  lcfrlem4  40416  lcfrlem6  40418  lcfrlem16  40429  lcdvsubval  40489  lcdlkreqN  40493  mapdcl2  40527  mapdincl  40532  mapdlsmcl  40534  mapdpglem3  40546  hdmaprnlem9N  40728  hdmaplkr  40784  hdmapip0  40786  hdmapglem7a  40798  sticksstones11  40972  sticksstones12a  40973  sticksstones19  40981  evlsscaval  41136  selvvvval  41157  evlselv  41159  mhphf2  41170  mhphf4  41172  prjspnvs  41362  prjspnn0  41364  prjspner1  41368  fltnltalem  41404  diophin  41510  acongeq  41722  isnumbasgrplem2  41846  proot1mul  41941  oacl2g  42080  omabs2  42082  omcl2  42083  iunrelexpuztr  42470  ntrclsiex  42804  ntrneiiex  42827  ntrneinex  42828  elnelneqd  42954  grurankcld  42992  bccbc  43104  suctrALT  43587  restuni3  43807  disjf1o  43889  disjinfi  43891  choicefi  43899  fsneq  43905  fsneqrn  43910  unirnmapsn  43913  iunmapsn  43916  monoords  44007  elfzolem1  44031  uzfissfz  44036  monoord2xrv  44194  evthiccabs  44209  iooabslt  44212  tgqioo2  44260  islptre  44335  limciccioolb  44337  sumnnodd  44346  limcicciooub  44353  lptre2pt  44356  limcresiooub  44358  limcresioolb  44359  lptioo1cn  44362  reclimc  44369  liminfvalxr  44499  liminfvaluz  44508  limsupvaluz3  44514  fsumcncf  44594  ioccncflimc  44601  cncfuni  44602  icccncfext  44603  cncficcgt0  44604  icocncflimc  44605  cncfdmsn  44606  cncfiooicclem1  44609  cncfiooicc  44610  cncfioobd  44613  cxpcncf2  44615  fprodsub2cncf  44621  fprodadd2cncf  44622  fperdvper  44635  dvcosax  44642  dvnmul  44659  dvnprodlem1  44662  dvnprodlem2  44663  itgsubsticclem  44691  fvvolioof  44705  fvvolicof  44707  stoweidlem26  44742  stoweidlem27  44743  stoweidlem31  44747  stoweidlem34  44750  dirkercncflem2  44820  dirkercncflem3  44821  dirkercncflem4  44822  dirkercncf  44823  fourierdlem16  44839  fourierdlem20  44843  fourierdlem21  44844  fourierdlem22  44845  fourierdlem26  44849  fourierdlem32  44855  fourierdlem33  44856  fourierdlem38  44861  fourierdlem39  44862  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem53  44875  fourierdlem60  44882  fourierdlem61  44883  fourierdlem69  44891  fourierdlem70  44892  fourierdlem71  44893  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem80  44902  fourierdlem81  44903  fourierdlem82  44904  fourierdlem83  44905  fourierdlem84  44906  fourierdlem85  44907  fourierdlem88  44910  fourierdlem89  44911  fourierdlem91  44913  fourierdlem92  44914  fourierdlem93  44915  fourierdlem100  44922  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem107  44929  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  fouriersw  44947  fouriercn  44948  etransclem24  44974  etransclem26  44976  etransclem28  44978  etransclem31  44981  etransclem32  44982  etransclem33  44983  etransclem34  44984  etransclem35  44985  etransclem38  44988  rrxtopnfi  45003  rrxtoponfi  45007  qndenserrnbl  45011  qndenserrnopnlem  45013  qndenserrn  45015  rrnprjdstle  45017  ioorrnopnlem  45020  prsal  45034  intsaluni  45045  salgencntex  45059  subsaliuncllem  45073  fge0iccico  45086  sge0sn  45095  sge0tsms  45096  sge0cl  45097  sge0f1o  45098  sge0pr  45110  sge0isum  45143  nnfoctbdjlem  45171  iundjiunlem  45175  iundjiun  45176  meadjiunlem  45181  psmeasure  45187  meaiininclem  45202  caragenelss  45217  omeunile  45221  carageniuncllem1  45237  carageniuncllem2  45238  0ome  45245  isomenndlem  45246  isomennd  45247  hoicvr  45264  ovnpnfelsup  45275  ovncvrrp  45280  ovnsubaddlem1  45286  hoidmv1le  45310  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  hoidmvle  45316  ovnhoilem1  45317  hoi2toco  45323  ovncvr2  45327  hspdifhsp  45332  voncmpl  45337  hoiqssbl  45341  hspmbllem2  45343  hspmbl  45345  hoimbllem  45346  opnvonmbllem2  45349  mblvon  45355  ovolval3  45363  ovolval4lem1  45365  ovnovollem1  45372  ovnovollem2  45373  vonsn  45407  issmflem  45443  sssmf  45454  issmflelem  45460  issmfgtlem  45471  issmfgt  45472  smfaddlem1  45479  issmfgelem  45485  smflimlem3  45489  smfmullem2  45508  smfmullem4  45510  smfsuplem1  45527  smfsupmpt  45531  smfinfmpt  45535  smflimsuplem2  45537  smflimsuplem4  45539  smflimsupmpt  45545  smfliminfmpt  45548  fsupdm  45558  finfdm  45562  fzoopth  46035  issubmgm2  46560  rngpropd  46673  imasrng  46678  subrngmcl  46736  rngqiprngimf  46782  rngqiprngimfo  46786  rngqiprngfulem4  46799  zlmodzxzel  47031  ply1mulgsum  47071  catprs  47631  thincmod  47651  mndtcob  47708  mndtccatid  47713  mndtcid  47715  grptcmon  47716  grptcepi  47717