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 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 2707

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

This theorem is referenced by:  eleqtrrd  2837  eleqtrid  2840  eleqtrdi  2844  3eltr3d  2848  prel12g  4840  opth1  5450  0nelop  5471  fvelimad  6945  fviss  6955  feldmfvelcdm  7075  tfisi  7852  fnwelem  8128  frrlem8  8290  frrlem10  8292  fprresex  8307  wfrlem17OLD  8337  omeulem1  8592  oeeulem  8611  oeeui  8612  oaabs2  8659  omabs  8661  ercl  8728  erth  8768  ecelqsdm  8799  ordtypelem6  9535  ordtypelem7  9536  cantnfval  9680  cantnfp1lem3  9692  cantnflem4  9704  r1pwss  9796  rankonidlem  9840  rankxplim3  9893  fseqenlem2  10037  iunfictbso  10126  dfac12lem1  10156  dfac12lem2  10157  fin23lem30  10354  iundom2g  10552  fpwwe2lem5  10647  fpwwe2lem8  10650  lincmb01cmp  13510  fzopth  13576  elfzolem1  13719  fzoaddel2  13734  fzosubel2  13739  fzocatel  13743  zpnn0elfzo1  13753  fzoend  13771  fzoopth  13776  peano2fzor  13788  monoord2  14049  sermono  14050  expmulnbnd  14251  bcpasc  14337  hash1elsn  14387  swrdcl  14661  revcl  14777  revlen  14778  fsum0diag2  15797  isumsplit  15854  fprodser  15963  sadadd  16484  sadass  16488  smuval2  16499  smumul  16510  vdwapun  16992  vdwlem9  17007  ramub1lem1  17044  prdsbasfn  17483  prdsbasprj  17484  pwsplusgval  17502  pwsmulrval  17503  pwsvscafval  17506  xpsaddlem  17585  xpsvsca  17589  xpsle  17591  mreexmrid  17653  homfeqval  17707  comfval2  17713  comfeq  17716  comfeqval  17718  oppccomfpropd  17737  invco  17782  sectepi  17795  issubc3  17860  funcf2  17879  fthepi  17941  nat1st2nd  17965  homarcl2  18046  coapm  18082  setcmon  18098  setcepi  18099  setcsect  18100  setcinv  18101  setciso  18102  cat1lem  18107  catccatid  18117  resscatc  18120  catciso  18122  catcbascl  18123  catcoppccl  18128  catcfuccl  18129  xpccatid  18198  catcxpccl  18217  xpcpropd  18218  evlfcl  18232  curfpropd  18243  hofcl  18269  yonedalem3  18290  yonffthlem  18292  poslubdg  18422  grpidd  18647  gsumress  18658  issubmgm2  18679  sgrppropd  18707  ismndd  18732  mndpropd  18735  issubmnd  18737  submnd0  18739  imasmnd  18751  xpsmnd0  18754  frmdelbas  18829  grpidd2  18958  pwsinvg  19034  imasgrp  19037  xpsinv  19041  xpsgrpsub  19042  ressmulgnnd  19059  submmulg  19099  subginvcl  19116  subgcl  19117  subgsub  19119  subgmulg  19121  1nsgtrivd  19155  quseccl0  19166  kerf1ghm  19228  ghmqusnsglem1  19261  ghmquskerlem1  19264  ghmquskerco  19265  ghmqusker  19268  gaid2  19284  finodsubmsubg  19546  submod  19548  odsubdvds  19550  sylow1lem4  19580  sylow2alem2  19597  lsmdisj2  19661  subgdisj1  19670  pj1id  19678  efgsrel  19713  efgrelexlemb  19729  efgcpbl2  19736  frgpcpbl  19738  frgp0  19739  frgpeccl  19740  frgpadd  19742  frgpup3lem  19756  frgpnabllem1  19852  cycsubgcyg  19880  prdsgsum  19960  dprdfeq0  20003  dmdprdsplitlem  20018  dpjidcl  20039  pgpfac1lem3a  20057  pgpfac1lem4  20059  pgpfaclem1  20062  pgpfaclem2  20063  ablfaclem2  20067  simpgnsgeqd  20082  simpgnsgbid  20084  ablsimpnosubgd  20085  rngpropd  20132  imasrng  20135  ringurd  20143  ringidss  20235  ringpropd  20246  imasring  20288  xpsring1d  20291  qusring2  20292  lringuplu  20502  subrngmcl  20515  subrg1  20540  subrgdv  20547  subrgunit  20548  resrhm  20559  issubdrg  20738  lmodprop2d  20879  0lmhm  20996  lmhmpropd  21029  lspfixed  21087  lssacsex  21103  lbsextlem4  21120  quscrng  21242  qusmulcrng  21243  rhmqusnsg  21244  rngqiprngimf  21256  rngqiprngimfo  21260  rngqiprngfulem4  21273  znf1o  21510  freshmansdream  21533  psgnghm2  21539  elocv  21626  pjff  21670  frlmlss  21709  frlmsubgval  21723  frlmvscafval  21724  frlmvscavalb  21728  frlmvplusgscavalb  21729  frlmphl  21739  uvcresum  21751  frlmssuvc1  21752  frlmssuvc2  21753  frlmsslsp  21754  frlmup1  21756  sraassab  21826  assapropd  21830  psrelbas  21892  resspsrvsca  21935  subrgpsr  21936  psrascl  21937  mplcoe1  21993  mplbas2  21998  mplascl  22020  mplmon2cl  22024  mplmon2mul  22025  evlrhm  22052  mpfconst  22057  mhprcl  22079  mhpvscacl  22090  psdascl  22104  vr1cl2  22126  ply1lss  22130  ply1subrg  22131  psropprmul  22171  ply1chr  22242  evl1vsd  22280  evl1expd  22281  evl1gsumadd  22294  evl1gsummon  22301  evls1fpws  22305  evls1vsca  22309  asclply1subcl  22310  evls1maplmhm  22313  evl1maprhm  22315  ply1vscl  22320  matring  22379  matassa  22380  mat1  22383  mattposcl  22389  mavmulass  22485  mdetunilem9  22556  matinv  22613  cpmadugsumlemF  22812  cpmadugsumfi  22813  cpmidgsum2  22815  elcls3  23019  mreclatdemoBAD  23032  neiptopnei  23068  resstps  23123  ordtrest2lem  23139  ordtrest2  23140  pnfnei  23156  mnfnei  23157  iscnp2  23175  iscnp4  23199  cnrest2r  23223  lmcls  23238  lmcld  23239  cnt0  23282  cnhaus  23290  isreg2  23313  connclo  23351  1stccnp  23398  loclly  23423  lly1stc  23432  locfincmp  23462  unisngl  23463  comppfsc  23468  kgencmp2  23482  llycmpkgen2  23486  kgen2ss  23491  kgencn3  23494  pttoponconst  23533  txcls  23540  txbasval  23542  dfac14lem  23553  ptcn  23563  ptrescn  23575  txtube  23576  txcmplem1  23577  txlm  23584  txkgen  23588  xkopjcn  23592  cnmptkp  23616  xkoinjcn  23623  qtopkgen  23646  imastps  23657  isr0  23673  r0cld  23674  pt1hmeo  23742  ptuncnv  23743  ptunhmeo  23744  filintn0  23797  trnei  23828  flimfil  23905  flimopn  23911  fbflim2  23913  cnpflf2  23936  flfcnp  23940  flfcnp2  23943  fclsopn  23950  fcfnei  23971  cnpfcf  23977  flfcntr  23979  alexsublem  23980  ptcmplem3  23990  ptcmplem4  23991  cnextfres1  24004  tmdcn2  24025  tmdgsum  24031  tmdgsum2  24032  efmndtmd  24037  symgtgp  24042  tgphaus  24053  tgpt1  24054  qustgplem  24057  prdstmdd  24060  prdstgpd  24061  haustsms  24072  tsmscls  24074  tsmsmhm  24082  tsmsadd  24083  tgptsmscls  24086  tsmssplit  24088  restutop  24174  utopreg  24189  ressusp  24201  ucncn  24221  xmetunirn  24274  ressprdsds  24308  xpsdsval  24318  xblss2ps  24338  blbas  24367  mopntopon  24376  isxms2  24385  imasf1oxms  24426  imasf1oms  24427  prdsxmslem2  24466  tmsxpsval  24475  tngngp2  24589  tngngp  24591  tgioo  24733  metdseq0  24792  cncfmpt2f  24857  cncfcnvcn  24868  cnmptre  24870  cnheibor  24903  nmhmcn  25069  cvsdiv  25081  cvsdivcl  25082  cphsubrglem  25127  cphreccllem  25128  iscmet3  25243  relcmpcmet  25268  bcthlem4  25277  rrxds  25343  rrxvsca  25344  rrxplusgvscavalb  25345  rrxbasefi  25360  rrxmetfi  25362  minveclem4  25382  mulcncf  25396  ivthicc  25409  evthicc  25410  ovolicc2lem4  25471  ovolicc2lem5  25472  iunmbl2  25508  vitalilem3  25561  cncombf  25609  cnmbf  25610  dvres2lem  25861  cpncn  25888  cpnres  25889  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvcobr  25899  dvcobrOLD  25900  dvcjbr  25903  dvrec  25909  dvcnvlem  25930  dvlip2  25950  dvivth  25965  lhop2  25970  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  ftc1lem6  25998  mdegvscale  26030  mdegvsca  26031  fta1blem  26126  plyaddlem1  26168  plymullem1  26169  coeeulem  26179  tayl0  26319  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmdvlem3  26361  psercnlem2  26384  psercn  26386  efsubm  26510  cxpcn3  26708  loglesqrt  26721  efrlim  26929  efrlimOLD  26930  ppinprm  27112  chtnprm  27114  dchrptlem1  27225  dchrptlem2  27226  nodenselem5  27650  oldlim  27842  cofcutr  27875  addsproplem6  27924  negsproplem6  27982  mulsproplem13  28071  mulsproplem14  28072  noseqp1  28214  tgbtwnouttr2  28420  tgldim0eq  28428  tgifscgr  28433  iscgrglt  28439  ercgrg  28442  tgcgrxfr  28443  motcgrg  28469  tglngne  28475  tgcolg  28479  tgbtwnconn1lem2  28498  tgbtwnconn1lem3  28499  legtri3  28515  legbtwn  28519  ncolne1  28550  tgisline  28552  tglinethru  28561  coltr3  28573  colline  28574  tglowdim2ln  28576  mirinv  28591  miriso  28595  mirauto  28609  miduniq  28610  krippenlem  28615  midexlem  28617  ragperp  28642  footexALT  28643  footexlem2  28645  perpdragALT  28652  perpdrag  28653  colperpexlem1  28655  colperpexlem3  28657  mideulem2  28659  midex  28662  opphllem1  28672  opphllem3  28674  opphllem4  28675  hlpasch  28681  trgcopy  28729  f1otrg  28796  axlowdimlem16  28882  elntg  28909  eengtrkg  28911  eengtrkge  28912  clwwlkccatlem  29916  grpoidinv2  30442  grpoinv  30452  ubthlem2  30798  shuni  31227  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  fpwrelmap  32656  fzm1ne1  32711  fzom1ne1  32724  ccatf1  32870  swrdf1  32878  pfxchn  32935  chnind  32937  chnub  32938  subgmulgcld  32984  ressmulgnn0d  32985  gsummpt2d  32989  gsumhashmul  33001  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  odpmco  33043  pmtrcnel  33046  pmtrcnel2  33047  pmtrcnelor  33048  tocyc01  33075  trsp2cyc  33080  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem1  33083  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  cycpmconjv  33099  cycpmrn  33100  tocyccntz  33101  0ringcring  33193  rloccring  33211  rloc0g  33212  rloc1r  33213  isdrng4  33235  sdrgdvcl  33239  sdrginvcl  33240  fracfld  33248  lpirlidllpi  33335  pidlnz  33337  nsgmgc  33373  rhmquskerlem  33386  elrspunidl  33389  elrspunsn  33390  drngidl  33394  qsidomlem1  33413  mxidlirred  33433  drngmxidlr  33439  opprmxidlabs  33448  opprqusplusg  33450  opprqusmulr  33452  opprqusdrng  33454  qsdrngilem  33455  qsdrngi  33456  qsdrnglem2  33457  qsdrng  33458  qsfld  33459  idlsrg0g  33467  1arithidomlem2  33497  ressdeg1  33525  ressply1invg  33528  ressply1sub  33529  ressasclcl  33530  ply1degltlss  33552  gsummoncoe1fzo  33553  ig1pmindeg  33557  q1pvsca  33559  r1pvsca  33560  srasubrg  33570  drgextlsp  33579  matdim  33601  lbslsat  33602  ply1degltdimlem  33608  ply1degltdim  33609  lindsunlem  33610  lbsdiflsp0  33612  dimkerim  33613  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  fldexttr  33646  extdgmul  33651  extdg1id  33653  irngss  33674  irngnzply1lem  33677  irngnzply1  33678  irngnminplynz  33692  algextdeglem4  33700  algextdeglem8  33704  rtelextdg2lem  33706  rtelextdg2  33707  constrconj  33725  rspectopn  33844  zarclsiin  33848  zarmxt1  33857  rspectps  33860  rhmpreimacn  33862  ordtrest2NEWlem  33899  ordtrest2NEW  33900  lmxrge0  33929  nmmulg  33943  rrhcn  33974  esumadd  34034  esumaddf  34038  esumcocn  34057  measiuns  34194  mbfmco2  34243  dya2iocnrect  34259  omscl  34273  omsf  34274  oms0  34275  sibf0  34312  sibfof  34318  sitgaddlemb  34326  fibp1  34379  ccatmulgnn0dir  34520  cxpcncf1  34573  ftc2re  34576  fsum2dsub  34585  reprf  34590  reprsum  34591  bnj1450  35027  bnj1501  35044  revpfxsfxrev  35084  indispconn  35202  connpconn  35203  pconnpi1  35205  sconnpi1  35207  cvmsss2  35242  cvmliftmolem1  35249  cvmliftlem8  35260  cvmliftlem10  35262  cvmliftlem11  35263  cvmlift2lem9  35279  cvmlift2lem12  35282  cvmlift3lem7  35293  mrsubcv  35478  mrsubff  35480  mrsubccat  35486  elmrsubrn  35488  mrsubco  35489  mrsubvrs  35490  linethru  36117  ivthALT  36299  neibastop2  36325  filnetlem4  36345  weiunfr  36431  matunitlindflem2  37587  poimirlem1  37591  poimirlem2  37592  poimirlem8  37598  poimirlem9  37599  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimir  37623  broucube  37624  areacirclem4  37681  fdc  37715  isbnd3  37754  prdsbnd  37763  prdstotbnd  37764  prdsbnd2  37765  rrnequiv  37805  reheibor  37809  iscringd  37968  isfldidl  38038  eqvrelth  38575  eqlkr  39063  ldualvsubval  39121  dvalveclem  40990  dia2dimlem5  41033  dia2dimlem9  41037  tendoinvcl  41069  dvhgrp  41072  dvhlveclem  41073  dihpN  41301  dochsnkr2cl  41439  lcfl7lem  41464  lclkr  41498  lclkrs  41504  lcfrvalsnN  41506  lcfrlem4  41510  lcfrlem6  41512  lcfrlem16  41523  lcdvsubval  41583  lcdlkreqN  41587  mapdcl2  41621  mapdincl  41626  mapdlsmcl  41628  mapdpglem3  41640  hdmaprnlem9N  41822  hdmaplkr  41878  hdmapip0  41880  hdmapglem7a  41892  zndvdchrrhm  41931  remexz  42063  primrootspoweq0  42065  aks6d1c1p3  42069  aks6d1c1p5  42071  aks6d1c2lem4  42086  idomnnzpownz  42091  idomnnzgmulnz  42092  ringexp0nn  42093  aks6d1c5lem0  42094  aks6d1c5lem3  42096  aks6d1c5lem2  42097  aks6d1c5  42098  sticksstones11  42115  sticksstones12a  42116  sticksstones19  42124  aks6d1c6lem2  42130  aks6d1c6lem4  42132  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  aks6d1c6lem5  42136  aks5lem2  42146  ply1asclzrhval  42147  rhmpsr1  42523  evlsscaval  42534  selvvvval  42555  evlselv  42557  mhphf2  42568  mhphf4  42570  prjspnvs  42590  prjspnn0  42592  prjspner1  42596  fltnltalem  42632  diophin  42742  acongeq  42954  isnumbasgrplem2  43075  proot1mul  43165  oacl2g  43301  omabs2  43303  omcl2  43304  iunrelexpuztr  43690  ntrclsiex  44024  ntrneiiex  44047  ntrneinex  44048  elnelneqd  44173  grurankcld  44205  bccbc  44317  suctrALT  44798  restuni3  45090  disjf1o  45163  disjinfi  45164  choicefi  45172  fsneq  45178  fsneqrn  45183  unirnmapsn  45186  iunmapsn  45189  monoords  45274  uzfissfz  45301  monoord2xrv  45458  evthiccabs  45473  iooabslt  45476  tgqioo2  45524  islptre  45596  limciccioolb  45598  sumnnodd  45607  limcicciooub  45614  lptre2pt  45617  limcresiooub  45619  limcresioolb  45620  lptioo1cn  45623  reclimc  45630  liminfvalxr  45760  liminfvaluz  45769  limsupvaluz3  45775  fsumcncf  45855  ioccncflimc  45862  cncfuni  45863  icccncfext  45864  cncficcgt0  45865  icocncflimc  45866  cncfdmsn  45867  cncfiooicclem1  45870  cncfiooicc  45871  cncfioobd  45874  cxpcncf2  45876  fprodsub2cncf  45882  fprodadd2cncf  45883  fperdvper  45896  dvcosax  45903  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  itgsubsticclem  45952  fvvolioof  45966  fvvolicof  45968  stoweidlem26  46003  stoweidlem27  46004  stoweidlem31  46008  stoweidlem34  46011  dirkercncflem2  46081  dirkercncflem3  46082  dirkercncflem4  46083  dirkercncf  46084  fourierdlem16  46100  fourierdlem20  46104  fourierdlem21  46105  fourierdlem22  46106  fourierdlem26  46110  fourierdlem32  46116  fourierdlem33  46117  fourierdlem38  46122  fourierdlem39  46123  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem53  46136  fourierdlem60  46143  fourierdlem61  46144  fourierdlem69  46152  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem80  46163  fourierdlem81  46164  fourierdlem82  46165  fourierdlem83  46166  fourierdlem84  46167  fourierdlem85  46168  fourierdlem88  46171  fourierdlem89  46172  fourierdlem91  46174  fourierdlem92  46175  fourierdlem93  46176  fourierdlem100  46183  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem107  46190  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  fouriersw  46208  fouriercn  46209  etransclem24  46235  etransclem26  46237  etransclem28  46239  etransclem31  46242  etransclem32  46243  etransclem33  46244  etransclem34  46245  etransclem35  46246  etransclem38  46249  rrxtopnfi  46264  rrxtoponfi  46268  qndenserrnbl  46272  qndenserrnopnlem  46274  qndenserrn  46276  rrnprjdstle  46278  ioorrnopnlem  46281  prsal  46295  intsaluni  46306  salgencntex  46320  subsaliuncllem  46334  fge0iccico  46347  sge0sn  46356  sge0tsms  46357  sge0cl  46358  sge0f1o  46359  sge0pr  46371  sge0isum  46404  nnfoctbdjlem  46432  iundjiunlem  46436  iundjiun  46437  meadjiunlem  46442  psmeasure  46448  meaiininclem  46463  caragenelss  46478  omeunile  46482  carageniuncllem1  46498  carageniuncllem2  46499  0ome  46506  isomenndlem  46507  isomennd  46508  hoicvr  46525  ovnpnfelsup  46536  ovncvrrp  46541  ovnsubaddlem1  46547  hoidmv1le  46571  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  hoidmvle  46577  ovnhoilem1  46578  hoi2toco  46584  ovncvr2  46588  hspdifhsp  46593  voncmpl  46598  hoiqssbl  46602  hspmbllem2  46604  hspmbl  46606  hoimbllem  46607  opnvonmbllem2  46610  mblvon  46616  ovolval3  46624  ovolval4lem1  46626  ovnovollem1  46633  ovnovollem2  46634  vonsn  46668  issmflem  46704  sssmf  46715  issmflelem  46721  issmfgtlem  46732  issmfgt  46733  smfaddlem1  46740  issmfgelem  46746  smflimlem3  46750  smfmullem2  46769  smfmullem4  46771  smfsuplem1  46788  smfsupmpt  46792  smfinfmpt  46796  smflimsuplem2  46798  smflimsuplem4  46800  smflimsupmpt  46806  smfliminfmpt  46809  fsupdm  46819  finfdm  46823  ormkglobd  46852  difltmodne  47319  zlmodzxzel  48278  ply1mulgsum  48314  catprs  48934  sectpropdlem  48951  invpropdlem  48953  isopropdlem  48955  cicpropdlem  48964  iinfsubc  48973  discsubc  48979  iinfconstbas  48981  ssccatid  48987  funchomf  49005  idfu1a  49009  idfu2nda  49010  imaf1co  49043  fthcomf  49045  upeu4  49077  swapf2a  49136  fuco2eld2  49173  fucof21  49206  fucoco2  49217  thincmod  49264  oppcthinco  49273  oppcthinendcALT  49275  termcbas2  49315  termchomn0  49317  isinito3  49333  termcterm  49346  termcciso  49349  termccisoeu  49350  idfudiag1  49358  diag2f1olem  49369  oduoppcciso  49391  mndtcob  49407  mndtccatid  49412  mndtcid  49414  grptcmon  49418  grptcepi  49419  2arwcat  49425  lanrcl  49444  ranrcl  49445  rellan  49446  relran  49447  islan  49448  isran  49451  lanrcl5  49457  ranrcl5  49462  concl  49479  coccl  49480