Theorem eleqtrd 2841

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  eleqtrrd  2842  eleqtrid  2845  eleqtrdi  2849  3eltr3d  2853  prel12g  4791  opth1  5384  0nelop  5404  fvelimad  6818  fviss  6827  tfisi  7680  fnwelem  7943  frrlem8  8080  frrlem10  8082  fprresex  8097  wfrlem17OLD  8127  omeulem1  8375  oeeulem  8394  oeeui  8395  oaabs2  8439  omabs  8441  ercl  8467  erth  8505  ecelqsdm  8534  ordtypelem6  9212  ordtypelem7  9213  cantnfval  9356  cantnfp1lem3  9368  cantnflem4  9380  r1pwss  9473  rankonidlem  9517  rankxplim3  9570  fseqenlem2  9712  iunfictbso  9801  dfac12lem1  9830  dfac12lem2  9831  fin23lem30  10029  iundom2g  10227  fpwwe2lem5  10322  fpwwe2lem8  10325  lincmb01cmp  13156  fzopth  13222  fzoaddel2  13371  fzosubel2  13375  fzocatel  13379  zpnn0elfzo1  13389  fzoend  13406  peano2fzor  13422  monoord2  13682  sermono  13683  expmulnbnd  13878  bcpasc  13963  hash1elsn  14014  swrdcl  14286  revcl  14402  revlen  14403  fsum0diag2  15423  isumsplit  15480  fprodser  15587  sadadd  16102  sadass  16106  smuval2  16117  smumul  16128  vdwapun  16603  vdwlem9  16618  ramub1lem1  16655  prdsbasfn  17099  prdsbasprj  17100  pwsplusgval  17118  pwsmulrval  17119  pwsvscafval  17122  xpsaddlem  17201  xpsvsca  17205  xpsle  17207  mreexmrid  17269  homfeqval  17323  comfval2  17329  comfeq  17332  comfeqval  17334  oppccomfpropd  17355  invco  17400  sectepi  17413  issubc3  17480  funcf2  17499  fthepi  17560  nat1st2nd  17583  homarcl2  17666  coapm  17702  setcmon  17718  setcepi  17719  setcsect  17720  setcinv  17721  setciso  17722  cat1lem  17727  catccatid  17737  resscatc  17740  catciso  17742  catcbascl  17743  catcoppccl  17748  catcoppcclOLD  17749  catcfuccl  17750  catcfucclOLD  17751  xpccatid  17821  catcxpccl  17840  catcxpcclOLD  17841  xpcpropd  17842  evlfcl  17856  curfpropd  17867  hofcl  17893  yonedalem3  17914  yonffthlem  17916  poslubdg  18047  grpidd  18270  gsumress  18281  ismndd  18322  mndpropd  18325  issubmnd  18327  submnd0  18329  imasmnd  18338  frmdelbas  18407  grpidd2  18532  pwsinvg  18603  imasgrp  18606  submmulg  18662  subginvcl  18679  subgcl  18680  subgsub  18682  subgmulg  18684  1nsgtrivd  18717  quseccl  18727  gaid2  18824  submod  19089  odsubdvds  19091  sylow1lem4  19121  sylow2alem2  19138  lsmdisj2  19203  subgdisj1  19212  pj1id  19220  efgsrel  19255  efgrelexlemb  19271  efgcpbl2  19278  frgpcpbl  19280  frgp0  19281  frgpeccl  19282  frgpadd  19284  frgpup3lem  19298  frgpnabllem1  19389  cycsubgcyg  19417  prdsgsum  19497  dprdfeq0  19540  dmdprdsplitlem  19555  dpjidcl  19576  pgpfac1lem3a  19594  pgpfac1lem4  19596  pgpfaclem1  19599  pgpfaclem2  19600  ablfaclem2  19604  simpgnsgeqd  19619  simpgnsgbid  19621  ablsimpnosubgd  19622  ringidss  19731  ringpropd  19736  imasring  19773  qusring2  19774  kerf1ghm  19902  subrg1  19949  subrgmcl  19951  subrgdv  19956  subrgunit  19957  issubdrg  19964  resrhm  19968  lmodprop2d  20100  0lmhm  20217  lmhmpropd  20250  lspfixed  20305  lssacsex  20321  lbsextlem4  20338  quscrng  20424  znf1o  20671  psgnghm2  20698  elocv  20785  pjff  20829  frlmlss  20868  frlmsubgval  20882  frlmvscafval  20883  frlmvscavalb  20887  frlmvplusgscavalb  20888  frlmphl  20898  uvcresum  20910  frlmssuvc1  20911  frlmssuvc2  20912  frlmsslsp  20913  frlmup1  20915  assapropd  20986  psrelbas  21058  resspsrvsca  21097  subrgpsr  21098  mplcoe1  21148  mplbas2  21153  mplascl  21182  mplmon2cl  21186  mplmon2mul  21187  evlrhm  21216  mpfconst  21221  mhpvscacl  21254  vr1cl2  21274  ply1lss  21277  ply1subrg  21278  psropprmul  21319  evl1vsd  21420  evl1expd  21421  evl1gsumadd  21434  evl1gsummon  21441  matring  21500  matassa  21501  mat1  21504  mattposcl  21510  mavmulass  21606  mdetunilem9  21677  matinv  21734  cpmadugsumlemF  21933  cpmadugsumfi  21934  cpmidgsum2  21936  elcls3  22142  mreclatdemoBAD  22155  neiptopnei  22191  resstps  22246  ordtrest2lem  22262  ordtrest2  22263  pnfnei  22279  mnfnei  22280  iscnp2  22298  iscnp4  22322  cnrest2r  22346  lmcls  22361  lmcld  22362  cnt0  22405  cnhaus  22413  isreg2  22436  connclo  22474  1stccnp  22521  loclly  22546  lly1stc  22555  locfincmp  22585  unisngl  22586  comppfsc  22591  kgencmp2  22605  llycmpkgen2  22609  kgen2ss  22614  kgencn3  22617  pttoponconst  22656  txcls  22663  txbasval  22665  dfac14lem  22676  ptcn  22686  ptrescn  22698  txtube  22699  txcmplem1  22700  txlm  22707  txkgen  22711  xkopjcn  22715  cnmptkp  22739  xkoinjcn  22746  qtopkgen  22769  imastps  22780  isr0  22796  r0cld  22797  pt1hmeo  22865  ptuncnv  22866  ptunhmeo  22867  filintn0  22920  trnei  22951  flimfil  23028  flimopn  23034  fbflim2  23036  cnpflf2  23059  flfcnp  23063  flfcnp2  23066  fclsopn  23073  fcfnei  23094  cnpfcf  23100  flfcntr  23102  alexsublem  23103  ptcmplem3  23113  ptcmplem4  23114  cnextfres1  23127  tmdcn2  23148  tmdgsum  23154  tmdgsum2  23155  efmndtmd  23160  symgtgp  23165  tgphaus  23176  tgpt1  23177  qustgplem  23180  prdstmdd  23183  prdstgpd  23184  haustsms  23195  tsmscls  23197  tsmsmhm  23205  tsmsadd  23206  tgptsmscls  23209  tsmssplit  23211  restutop  23297  utopreg  23312  ressusp  23324  ucncn  23345  xmetunirn  23398  ressprdsds  23432  xpsdsval  23442  xblss2ps  23462  blbas  23491  mopntopon  23500  isxms2  23509  imasf1oxms  23551  imasf1oms  23552  prdsxmslem2  23591  tmsxpsval  23600  tngngp2  23722  tngngp  23724  tgioo  23865  metdseq0  23923  cncfmpt2f  23984  cncfcnvcn  23994  cnmptre  23996  cnheibor  24024  nmhmcn  24189  cvsdiv  24201  cvsdivcl  24202  cphsubrglem  24246  cphreccllem  24247  iscmet3  24362  relcmpcmet  24387  bcthlem4  24396  rrxds  24462  rrxvsca  24463  rrxplusgvscavalb  24464  rrxbasefi  24479  rrxmetfi  24481  minveclem4  24501  ivthicc  24527  evthicc  24528  ovolicc2lem4  24589  ovolicc2lem5  24590  iunmbl2  24626  vitalilem3  24679  cncombf  24727  cnmbf  24728  dvres2lem  24979  cpncn  25005  cpnres  25006  dvaddbr  25007  dvmulbr  25008  dvcobr  25015  dvcjbr  25018  dvrec  25024  dvcnvlem  25045  dvlip2  25064  dvivth  25079  lhop2  25084  lhop  25085  dvcnvrelem1  25086  dvcnvrelem2  25087  dvcnvre  25088  ftc1lem6  25110  mdegvscale  25145  mdegvsca  25146  fta1blem  25238  plyaddlem1  25279  plymullem1  25280  coeeulem  25290  tayl0  25426  taylthlem1  25437  taylthlem2  25438  ulmdvlem3  25466  psercnlem2  25488  psercn  25490  efsubm  25612  cxpcn3  25806  loglesqrt  25816  efrlim  26024  ppinprm  26206  chtnprm  26208  dchrptlem1  26317  dchrptlem2  26318  tgbtwnouttr2  26760  tgldim0eq  26768  tgifscgr  26773  iscgrglt  26779  ercgrg  26782  tgcgrxfr  26783  motcgrg  26809  tglngne  26815  tgcolg  26819  tgbtwnconn1lem2  26838  tgbtwnconn1lem3  26839  legtri3  26855  legbtwn  26859  ncolne1  26890  tgisline  26892  tglinethru  26901  coltr3  26913  colline  26914  tglowdim2ln  26916  mirinv  26931  miriso  26935  mirauto  26949  miduniq  26950  krippenlem  26955  midexlem  26957  ragperp  26982  footexALT  26983  footexlem2  26985  perpdragALT  26992  perpdrag  26993  colperpexlem1  26995  colperpexlem3  26997  mideulem2  26999  midex  27002  opphllem1  27012  opphllem3  27014  opphllem4  27015  hlpasch  27021  trgcopy  27069  f1otrg  27136  axlowdimlem16  27228  elntg  27255  eengtrkg  27257  eengtrkge  27258  clwwlkccatlem  28254  grpoidinv2  28778  grpoinv  28788  ubthlem2  29134  shuni  29563  acunirnmpt  30898  acunirnmpt2  30899  acunirnmpt2f  30900  fpwrelmap  30970  fzm1ne1  31012  fzom1ne1  31024  ccatf1  31125  swrdf1  31130  gsummpt2d  31211  gsumhashmul  31218  odpmco  31257  pmtrcnel  31260  pmtrcnel2  31261  pmtrcnelor  31262  tocyc01  31287  trsp2cyc  31292  cycpmco2f1  31293  cycpmco2rn  31294  cycpmco2lem1  31295  cycpmco2lem2  31296  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  cycpmconjv  31311  cycpmrn  31312  tocyccntz  31313  rngurd  31384  freshmansdream  31386  pidlnz  31473  nsgmgc  31499  elrspunidl  31508  qsidomlem1  31530  idlsrg0g  31553  ply1chr  31571  srasubrg  31576  drgextlsp  31583  matdim  31600  lbslsat  31601  lindsunlem  31607  lbsdiflsp0  31609  dimkerim  31610  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  fldexttr  31635  extdgmul  31638  extdg1id  31640  rspectopn  31719  zarclsiin  31723  zarmxt1  31732  rspectps  31735  rhmpreimacn  31737  ordtrest2NEWlem  31774  ordtrest2NEW  31775  lmxrge0  31804  nmmulg  31818  rrhcn  31847  esumadd  31925  esumaddf  31929  esumcocn  31948  measiuns  32085  mbfmco2  32132  dya2iocnrect  32148  omscl  32162  omsf  32163  oms0  32164  sibf0  32201  sibfof  32207  sitgaddlemb  32215  fibp1  32268  ccatmulgnn0dir  32421  cxpcncf1  32475  ftc2re  32478  fsum2dsub  32487  reprf  32492  reprsum  32493  bnj1450  32930  bnj1501  32947  revpfxsfxrev  32977  indispconn  33096  connpconn  33097  pconnpi1  33099  sconnpi1  33101  cvmsss2  33136  cvmliftmolem1  33143  cvmliftlem8  33154  cvmliftlem10  33156  cvmliftlem11  33157  cvmlift2lem9  33173  cvmlift2lem12  33176  cvmlift3lem7  33187  mrsubcv  33372  mrsubff  33374  mrsubccat  33380  elmrsubrn  33382  mrsubco  33383  mrsubvrs  33384  nodenselem5  33818  oldlim  33996  cofcutr  34019  linethru  34382  ivthALT  34451  neibastop2  34477  filnetlem4  34497  matunitlindflem2  35701  poimirlem1  35705  poimirlem2  35706  poimirlem8  35712  poimirlem9  35713  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimir  35737  broucube  35738  areacirclem4  35795  fdc  35830  isbnd3  35869  prdsbnd  35878  prdstotbnd  35879  prdsbnd2  35880  rrnequiv  35920  reheibor  35924  iscringd  36083  isfldidl  36153  eqvrelth  36651  eqlkr  37040  ldualvsubval  37098  dvalveclem  38966  dia2dimlem5  39009  dia2dimlem9  39013  tendoinvcl  39045  dvhgrp  39048  dvhlveclem  39049  dihpN  39277  dochsnkr2cl  39415  lcfl7lem  39440  lclkr  39474  lclkrs  39480  lcfrvalsnN  39482  lcfrlem4  39486  lcfrlem6  39488  lcfrlem16  39499  lcdvsubval  39559  lcdlkreqN  39563  mapdcl2  39597  mapdincl  39602  mapdlsmcl  39604  mapdpglem3  39616  hdmaprnlem9N  39798  hdmaplkr  39854  hdmapip0  39856  hdmapglem7a  39868  sticksstones11  40040  sticksstones12a  40041  sticksstones19  40049  evlsscaval  40196  mhphf  40208  mhphf2  40209  prjspnvs  40380  prjspner1  40384  fltnltalem  40415  diophin  40510  acongeq  40721  isnumbasgrplem2  40845  proot1mul  40940  iunrelexpuztr  41216  ntrclsiex  41552  ntrneiiex  41575  ntrneinex  41576  elnelneqd  41702  grurankcld  41740  bccbc  41852  suctrALT  42335  restuni3  42556  disjf1o  42618  disjinfi  42620  choicefi  42629  fsneq  42635  fsneqrn  42640  unirnmapsn  42643  iunmapsn  42646  monoords  42726  elfzolem1  42750  uzfissfz  42755  monoord2xrv  42914  evthiccabs  42924  iooabslt  42927  tgqioo2  42975  islptre  43050  limciccioolb  43052  sumnnodd  43061  limcicciooub  43068  lptre2pt  43071  limcresiooub  43073  limcresioolb  43074  lptioo1cn  43077  reclimc  43084  liminfvalxr  43214  liminfvaluz  43223  limsupvaluz3  43229  fsumcncf  43309  ioccncflimc  43316  cncfuni  43317  icccncfext  43318  cncficcgt0  43319  icocncflimc  43320  cncfdmsn  43321  cncfiooicclem1  43324  cncfiooicc  43325  cncfioobd  43328  cxpcncf2  43330  fprodsub2cncf  43336  fprodadd2cncf  43337  fperdvper  43350  dvcosax  43357  dvnmul  43374  dvnprodlem1  43377  dvnprodlem2  43378  itgsubsticclem  43406  fvvolioof  43420  fvvolicof  43422  stoweidlem26  43457  stoweidlem27  43458  stoweidlem31  43462  stoweidlem34  43465  dirkercncflem2  43535  dirkercncflem3  43536  dirkercncflem4  43537  dirkercncf  43538  fourierdlem16  43554  fourierdlem20  43558  fourierdlem21  43559  fourierdlem22  43560  fourierdlem26  43564  fourierdlem32  43570  fourierdlem33  43571  fourierdlem38  43576  fourierdlem39  43577  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem53  43590  fourierdlem60  43597  fourierdlem61  43598  fourierdlem69  43606  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem80  43617  fourierdlem81  43618  fourierdlem82  43619  fourierdlem83  43620  fourierdlem84  43621  fourierdlem85  43622  fourierdlem88  43625  fourierdlem89  43626  fourierdlem91  43628  fourierdlem92  43629  fourierdlem93  43630  fourierdlem100  43637  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fouriersw  43662  fouriercn  43663  etransclem24  43689  etransclem26  43691  etransclem28  43693  etransclem31  43696  etransclem32  43697  etransclem33  43698  etransclem34  43699  etransclem35  43700  etransclem38  43703  rrxtopnfi  43718  rrxtoponfi  43722  qndenserrnbl  43726  qndenserrnopnlem  43728  qndenserrn  43730  rrnprjdstle  43732  ioorrnopnlem  43735  prsal  43749  intsaluni  43758  salgencntex  43772  subsaliuncllem  43786  fge0iccico  43798  sge0sn  43807  sge0tsms  43808  sge0cl  43809  sge0f1o  43810  sge0pr  43822  sge0isum  43855  nnfoctbdjlem  43883  iundjiunlem  43887  iundjiun  43888  meadjiunlem  43893  psmeasure  43899  meaiininclem  43914  caragenelss  43929  omeunile  43933  carageniuncllem1  43949  carageniuncllem2  43950  0ome  43957  isomenndlem  43958  isomennd  43959  hoicvr  43976  ovnpnfelsup  43987  ovncvrrp  43992  ovnsubaddlem1  43998  hoidmv1le  44022  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvle  44028  ovnhoilem1  44029  hoi2toco  44035  ovncvr2  44039  hspdifhsp  44044  voncmpl  44049  hoiqssbl  44053  hspmbllem2  44055  hspmbl  44057  hoimbllem  44058  opnvonmbllem2  44061  mblvon  44067  ovolval3  44075  ovolval4lem1  44077  ovnovollem1  44084  ovnovollem2  44085  vonsn  44119  issmflem  44150  sssmf  44161  issmflelem  44167  issmfgtlem  44178  issmfgt  44179  smfaddlem1  44185  issmfgelem  44191  smflimlem3  44195  smfmullem2  44213  smfmullem4  44215  smfsuplem1  44231  smfsupmpt  44235  smfinfmpt  44239  smflimsuplem2  44241  smflimsuplem4  44243  smflimsupmpt  44249  smfliminfmpt  44252  fzoopth  44707  issubmgm2  45232  zlmodzxzel  45579  ply1mulgsum  45619  catprs  46180  thincmod  46200  mndtcob  46255  mndtccatid  46260  mndtcid  46262  grptcmon  46263  grptcepi  46264