Theorem eleqtrd 2833

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

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

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808

This theorem is referenced by:  eleqtrrd  2834  eleqtrid  2837  eleqtrdi  2841  3eltr3d  2845  prel12g  4863  opth1  5474  0nelop  5495  fvelimad  6958  fviss  6967  tfisi  7850  fnwelem  8119  frrlem8  8280  frrlem10  8282  fprresex  8297  wfrlem17OLD  8327  omeulem1  8584  oeeulem  8603  oeeui  8604  oaabs2  8650  omabs  8652  ercl  8716  erth  8754  ecelqsdm  8783  ordtypelem6  9520  ordtypelem7  9521  cantnfval  9665  cantnfp1lem3  9677  cantnflem4  9689  r1pwss  9781  rankonidlem  9825  rankxplim3  9878  fseqenlem2  10022  iunfictbso  10111  dfac12lem1  10140  dfac12lem2  10141  fin23lem30  10339  iundom2g  10537  fpwwe2lem5  10632  fpwwe2lem8  10635  lincmb01cmp  13476  fzopth  13542  fzoaddel2  13692  fzosubel2  13696  fzocatel  13700  zpnn0elfzo1  13710  fzoend  13727  peano2fzor  13743  monoord2  14003  sermono  14004  expmulnbnd  14202  bcpasc  14285  hash1elsn  14335  swrdcl  14599  revcl  14715  revlen  14716  fsum0diag2  15733  isumsplit  15790  fprodser  15897  sadadd  16412  sadass  16416  smuval2  16427  smumul  16438  vdwapun  16911  vdwlem9  16926  ramub1lem1  16963  prdsbasfn  17421  prdsbasprj  17422  pwsplusgval  17440  pwsmulrval  17441  pwsvscafval  17444  xpsaddlem  17523  xpsvsca  17527  xpsle  17529  mreexmrid  17591  homfeqval  17645  comfval2  17651  comfeq  17654  comfeqval  17656  oppccomfpropd  17677  invco  17722  sectepi  17735  issubc3  17803  funcf2  17822  fthepi  17883  nat1st2nd  17906  homarcl2  17989  coapm  18025  setcmon  18041  setcepi  18042  setcsect  18043  setcinv  18044  setciso  18045  cat1lem  18050  catccatid  18060  resscatc  18063  catciso  18065  catcbascl  18066  catcoppccl  18071  catcoppcclOLD  18072  catcfuccl  18073  catcfucclOLD  18074  xpccatid  18144  catcxpccl  18163  catcxpcclOLD  18164  xpcpropd  18165  evlfcl  18179  curfpropd  18190  hofcl  18216  yonedalem3  18237  yonffthlem  18239  poslubdg  18371  grpidd  18596  gsumress  18607  issubmgm2  18628  sgrppropd  18656  ismndd  18681  mndpropd  18684  issubmnd  18686  submnd0  18688  imasmnd  18697  xpsmnd0  18700  frmdelbas  18770  grpidd2  18898  pwsinvg  18972  imasgrp  18975  xpsinv  18979  xpsgrpsub  18980  submmulg  19034  subginvcl  19051  subgcl  19052  subgsub  19054  subgmulg  19056  1nsgtrivd  19090  quseccl0  19100  kerf1ghm  19161  gaid2  19208  finodsubmsubg  19476  submod  19478  odsubdvds  19480  sylow1lem4  19510  sylow2alem2  19527  lsmdisj2  19591  subgdisj1  19600  pj1id  19608  efgsrel  19643  efgrelexlemb  19659  efgcpbl2  19666  frgpcpbl  19668  frgp0  19669  frgpeccl  19670  frgpadd  19672  frgpup3lem  19686  frgpnabllem1  19782  cycsubgcyg  19810  prdsgsum  19890  dprdfeq0  19933  dmdprdsplitlem  19948  dpjidcl  19969  pgpfac1lem3a  19987  pgpfac1lem4  19989  pgpfaclem1  19992  pgpfaclem2  19993  ablfaclem2  19997  simpgnsgeqd  20012  simpgnsgbid  20014  ablsimpnosubgd  20015  rngpropd  20068  imasrng  20071  ringurd  20079  ringidss  20165  ringpropd  20176  imasring  20218  xpsring1d  20221  qusring2  20222  lringuplu  20432  subrngmcl  20445  subrg1  20472  subrgdv  20479  subrgunit  20480  resrhm  20491  issubdrg  20544  lmodprop2d  20678  0lmhm  20795  lmhmpropd  20828  lspfixed  20886  lssacsex  20902  lbsextlem4  20919  quscrng  21029  rngqiprngimf  21056  rngqiprngimfo  21060  rngqiprngfulem4  21073  znf1o  21326  psgnghm2  21353  elocv  21440  pjff  21486  frlmlss  21525  frlmsubgval  21539  frlmvscafval  21540  frlmvscavalb  21544  frlmvplusgscavalb  21545  frlmphl  21555  uvcresum  21567  frlmssuvc1  21568  frlmssuvc2  21569  frlmsslsp  21570  frlmup1  21572  sraassab  21641  assapropd  21645  psrelbas  21717  resspsrvsca  21757  subrgpsr  21758  mplcoe1  21811  mplbas2  21816  mplascl  21844  mplmon2cl  21848  mplmon2mul  21849  evlrhm  21878  mpfconst  21883  mhpvscacl  21916  vr1cl2  21936  ply1lss  21939  ply1subrg  21940  psropprmul  21980  evl1vsd  22083  evl1expd  22084  evl1gsumadd  22097  evl1gsummon  22104  matring  22165  matassa  22166  mat1  22169  mattposcl  22175  mavmulass  22271  mdetunilem9  22342  matinv  22399  cpmadugsumlemF  22598  cpmadugsumfi  22599  cpmidgsum2  22601  elcls3  22807  mreclatdemoBAD  22820  neiptopnei  22856  resstps  22911  ordtrest2lem  22927  ordtrest2  22928  pnfnei  22944  mnfnei  22945  iscnp2  22963  iscnp4  22987  cnrest2r  23011  lmcls  23026  lmcld  23027  cnt0  23070  cnhaus  23078  isreg2  23101  connclo  23139  1stccnp  23186  loclly  23211  lly1stc  23220  locfincmp  23250  unisngl  23251  comppfsc  23256  kgencmp2  23270  llycmpkgen2  23274  kgen2ss  23279  kgencn3  23282  pttoponconst  23321  txcls  23328  txbasval  23330  dfac14lem  23341  ptcn  23351  ptrescn  23363  txtube  23364  txcmplem1  23365  txlm  23372  txkgen  23376  xkopjcn  23380  cnmptkp  23404  xkoinjcn  23411  qtopkgen  23434  imastps  23445  isr0  23461  r0cld  23462  pt1hmeo  23530  ptuncnv  23531  ptunhmeo  23532  filintn0  23585  trnei  23616  flimfil  23693  flimopn  23699  fbflim2  23701  cnpflf2  23724  flfcnp  23728  flfcnp2  23731  fclsopn  23738  fcfnei  23759  cnpfcf  23765  flfcntr  23767  alexsublem  23768  ptcmplem3  23778  ptcmplem4  23779  cnextfres1  23792  tmdcn2  23813  tmdgsum  23819  tmdgsum2  23820  efmndtmd  23825  symgtgp  23830  tgphaus  23841  tgpt1  23842  qustgplem  23845  prdstmdd  23848  prdstgpd  23849  haustsms  23860  tsmscls  23862  tsmsmhm  23870  tsmsadd  23871  tgptsmscls  23874  tsmssplit  23876  restutop  23962  utopreg  23977  ressusp  23989  ucncn  24010  xmetunirn  24063  ressprdsds  24097  xpsdsval  24107  xblss2ps  24127  blbas  24156  mopntopon  24165  isxms2  24174  imasf1oxms  24218  imasf1oms  24219  prdsxmslem2  24258  tmsxpsval  24267  tngngp2  24389  tngngp  24391  tgioo  24532  metdseq0  24590  cncfmpt2f  24655  cncfcnvcn  24666  cnmptre  24668  cnheibor  24701  nmhmcn  24867  cvsdiv  24879  cvsdivcl  24880  cphsubrglem  24925  cphreccllem  24926  iscmet3  25041  relcmpcmet  25066  bcthlem4  25075  rrxds  25141  rrxvsca  25142  rrxplusgvscavalb  25143  rrxbasefi  25158  rrxmetfi  25160  minveclem4  25180  mulcncf  25194  ivthicc  25207  evthicc  25208  ovolicc2lem4  25269  ovolicc2lem5  25270  iunmbl2  25306  vitalilem3  25359  cncombf  25407  cnmbf  25408  dvres2lem  25659  cpncn  25686  cpnres  25687  dvaddbr  25688  dvmulbr  25689  dvmulbrOLD  25690  dvcobr  25697  dvcobrOLD  25698  dvcjbr  25701  dvrec  25707  dvcnvlem  25728  dvlip2  25747  dvivth  25762  lhop2  25767  lhop  25768  dvcnvrelem1  25769  dvcnvrelem2  25770  dvcnvre  25771  ftc1lem6  25793  mdegvscale  25828  mdegvsca  25829  fta1blem  25921  plyaddlem1  25962  plymullem1  25963  coeeulem  25973  tayl0  26110  taylthlem1  26121  taylthlem2  26122  ulmdvlem3  26150  psercnlem2  26172  psercn  26174  efsubm  26296  cxpcn3  26492  loglesqrt  26502  efrlim  26710  ppinprm  26892  chtnprm  26894  dchrptlem1  27003  dchrptlem2  27004  nodenselem5  27427  oldlim  27618  cofcutr  27649  addsproplem6  27696  negsproplem6  27746  mulsproplem13  27823  mulsproplem14  27824  tgbtwnouttr2  28013  tgldim0eq  28021  tgifscgr  28026  iscgrglt  28032  ercgrg  28035  tgcgrxfr  28036  motcgrg  28062  tglngne  28068  tgcolg  28072  tgbtwnconn1lem2  28091  tgbtwnconn1lem3  28092  legtri3  28108  legbtwn  28112  ncolne1  28143  tgisline  28145  tglinethru  28154  coltr3  28166  colline  28167  tglowdim2ln  28169  mirinv  28184  miriso  28188  mirauto  28202  miduniq  28203  krippenlem  28208  midexlem  28210  ragperp  28235  footexALT  28236  footexlem2  28238  perpdragALT  28245  perpdrag  28246  colperpexlem1  28248  colperpexlem3  28250  mideulem2  28252  midex  28255  opphllem1  28265  opphllem3  28267  opphllem4  28268  hlpasch  28274  trgcopy  28322  f1otrg  28389  axlowdimlem16  28482  elntg  28509  eengtrkg  28511  eengtrkge  28512  clwwlkccatlem  29509  grpoidinv2  30035  grpoinv  30045  ubthlem2  30391  shuni  30820  acunirnmpt  32151  acunirnmpt2  32152  acunirnmpt2f  32153  fpwrelmap  32225  fzm1ne1  32267  fzom1ne1  32279  ccatf1  32382  swrdf1  32387  gsummpt2d  32471  gsumhashmul  32478  odpmco  32517  pmtrcnel  32520  pmtrcnel2  32521  pmtrcnelor  32522  tocyc01  32547  trsp2cyc  32552  cycpmco2f1  32553  cycpmco2rn  32554  cycpmco2lem1  32555  cycpmco2lem2  32556  cycpmco2lem3  32557  cycpmco2lem4  32558  cycpmco2lem5  32559  cycpmco2lem6  32560  cycpmco2lem7  32561  cycpmco2  32562  cycpmconjv  32571  cycpmrn  32572  tocyccntz  32573  freshmansdream  32651  isdrng4  32665  sdrgdvcl  32667  sdrginvcl  32668  pidlnz  32762  qusmul  32789  nsgmgc  32797  ghmquskerlem1  32802  ghmquskerco  32803  ghmqusker  32806  rhmquskerlem  32817  elrspunidl  32820  elrspunsn  32821  drngidl  32825  qsidomlem1  32845  mxidlirred  32862  opprmxidlabs  32875  opprqusplusg  32877  opprqusmulr  32879  opprqusdrng  32881  qsdrngilem  32882  qsdrngi  32883  qsdrnglem2  32884  qsdrng  32885  qsfld  32886  idlsrg0g  32894  evls1fpws  32920  evls1vsca  32924  ressdeg1  32925  ressply1invg  32932  ressply1sub  32933  asclply1subcl  32934  ply1chr  32935  ply1degltlss  32942  gsummoncoe1fzo  32943  ig1pmindeg  32947  q1pvsca  32949  r1pvsca  32950  srasubrg  32959  drgextlsp  32968  matdim  32988  lbslsat  32989  ply1degltdimlem  32995  ply1degltdim  32996  lindsunlem  32997  lbsdiflsp0  32999  dimkerim  33000  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  fldexttr  33025  extdgmul  33028  extdg1id  33030  irngss  33040  irngnzply1lem  33043  irngnzply1  33044  evls1maplmhm  33049  irngnminplynz  33060  algextdeglem4  33065  algextdeglem8  33069  rspectopn  33145  zarclsiin  33149  zarmxt1  33158  rspectps  33161  rhmpreimacn  33163  ordtrest2NEWlem  33200  ordtrest2NEW  33201  lmxrge0  33230  nmmulg  33246  rrhcn  33275  esumadd  33353  esumaddf  33357  esumcocn  33376  measiuns  33513  mbfmco2  33562  dya2iocnrect  33578  omscl  33592  omsf  33593  oms0  33594  sibf0  33631  sibfof  33637  sitgaddlemb  33645  fibp1  33698  ccatmulgnn0dir  33851  cxpcncf1  33905  ftc2re  33908  fsum2dsub  33917  reprf  33922  reprsum  33923  bnj1450  34359  bnj1501  34376  revpfxsfxrev  34404  indispconn  34523  connpconn  34524  pconnpi1  34526  sconnpi1  34528  cvmsss2  34563  cvmliftmolem1  34570  cvmliftlem8  34581  cvmliftlem10  34583  cvmliftlem11  34584  cvmlift2lem9  34600  cvmlift2lem12  34603  cvmlift3lem7  34614  mrsubcv  34799  mrsubff  34801  mrsubccat  34807  elmrsubrn  34809  mrsubco  34810  mrsubvrs  34811  linethru  35429  ivthALT  35523  neibastop2  35549  filnetlem4  35569  matunitlindflem2  36788  poimirlem1  36792  poimirlem2  36793  poimirlem8  36799  poimirlem9  36800  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem22  36813  poimirlem23  36814  poimir  36824  broucube  36825  areacirclem4  36882  fdc  36916  isbnd3  36955  prdsbnd  36964  prdstotbnd  36965  prdsbnd2  36966  rrnequiv  37006  reheibor  37010  iscringd  37169  isfldidl  37239  eqvrelth  37784  eqlkr  38272  ldualvsubval  38330  dvalveclem  40199  dia2dimlem5  40242  dia2dimlem9  40246  tendoinvcl  40278  dvhgrp  40281  dvhlveclem  40282  dihpN  40510  dochsnkr2cl  40648  lcfl7lem  40673  lclkr  40707  lclkrs  40713  lcfrvalsnN  40715  lcfrlem4  40719  lcfrlem6  40721  lcfrlem16  40732  lcdvsubval  40792  lcdlkreqN  40796  mapdcl2  40830  mapdincl  40835  mapdlsmcl  40837  mapdpglem3  40849  hdmaprnlem9N  41031  hdmaplkr  41087  hdmapip0  41089  hdmapglem7a  41101  sticksstones11  41278  sticksstones12a  41279  sticksstones19  41287  evlsscaval  41438  selvvvval  41459  evlselv  41461  mhphf2  41472  mhphf4  41474  prjspnvs  41664  prjspnn0  41666  prjspner1  41670  fltnltalem  41706  diophin  41812  acongeq  42024  isnumbasgrplem2  42148  proot1mul  42243  oacl2g  42382  omabs2  42384  omcl2  42385  iunrelexpuztr  42772  ntrclsiex  43106  ntrneiiex  43129  ntrneinex  43130  elnelneqd  43256  grurankcld  43294  bccbc  43406  suctrALT  43889  restuni3  44108  disjf1o  44188  disjinfi  44189  choicefi  44197  fsneq  44203  fsneqrn  44208  unirnmapsn  44211  iunmapsn  44214  monoords  44305  elfzolem1  44329  uzfissfz  44334  monoord2xrv  44492  evthiccabs  44507  iooabslt  44510  tgqioo2  44558  islptre  44633  limciccioolb  44635  sumnnodd  44644  limcicciooub  44651  lptre2pt  44654  limcresiooub  44656  limcresioolb  44657  lptioo1cn  44660  reclimc  44667  liminfvalxr  44797  liminfvaluz  44806  limsupvaluz3  44812  fsumcncf  44892  ioccncflimc  44899  cncfuni  44900  icccncfext  44901  cncficcgt0  44902  icocncflimc  44903  cncfdmsn  44904  cncfiooicclem1  44907  cncfiooicc  44908  cncfioobd  44911  cxpcncf2  44913  fprodsub2cncf  44919  fprodadd2cncf  44920  fperdvper  44933  dvcosax  44940  dvnmul  44957  dvnprodlem1  44960  dvnprodlem2  44961  itgsubsticclem  44989  fvvolioof  45003  fvvolicof  45005  stoweidlem26  45040  stoweidlem27  45041  stoweidlem31  45045  stoweidlem34  45048  dirkercncflem2  45118  dirkercncflem3  45119  dirkercncflem4  45120  dirkercncf  45121  fourierdlem16  45137  fourierdlem20  45141  fourierdlem21  45142  fourierdlem22  45143  fourierdlem26  45147  fourierdlem32  45153  fourierdlem33  45154  fourierdlem38  45159  fourierdlem39  45160  fourierdlem46  45166  fourierdlem48  45168  fourierdlem49  45169  fourierdlem53  45173  fourierdlem60  45180  fourierdlem61  45181  fourierdlem69  45189  fourierdlem70  45190  fourierdlem71  45191  fourierdlem73  45193  fourierdlem74  45194  fourierdlem75  45195  fourierdlem76  45196  fourierdlem80  45200  fourierdlem81  45201  fourierdlem82  45202  fourierdlem83  45203  fourierdlem84  45204  fourierdlem85  45205  fourierdlem88  45208  fourierdlem89  45209  fourierdlem91  45211  fourierdlem92  45212  fourierdlem93  45213  fourierdlem100  45220  fourierdlem101  45221  fourierdlem103  45223  fourierdlem104  45224  fourierdlem107  45227  fourierdlem111  45231  fourierdlem112  45232  fourierdlem113  45233  fouriersw  45245  fouriercn  45246  etransclem24  45272  etransclem26  45274  etransclem28  45276  etransclem31  45279  etransclem32  45280  etransclem33  45281  etransclem34  45282  etransclem35  45283  etransclem38  45286  rrxtopnfi  45301  rrxtoponfi  45305  qndenserrnbl  45309  qndenserrnopnlem  45311  qndenserrn  45313  rrnprjdstle  45315  ioorrnopnlem  45318  prsal  45332  intsaluni  45343  salgencntex  45357  subsaliuncllem  45371  fge0iccico  45384  sge0sn  45393  sge0tsms  45394  sge0cl  45395  sge0f1o  45396  sge0pr  45408  sge0isum  45441  nnfoctbdjlem  45469  iundjiunlem  45473  iundjiun  45474  meadjiunlem  45479  psmeasure  45485  meaiininclem  45500  caragenelss  45515  omeunile  45519  carageniuncllem1  45535  carageniuncllem2  45536  0ome  45543  isomenndlem  45544  isomennd  45545  hoicvr  45562  ovnpnfelsup  45573  ovncvrrp  45578  ovnsubaddlem1  45584  hoidmv1le  45608  hoidmvlelem2  45610  hoidmvlelem3  45611  hoidmvlelem4  45612  hoidmvle  45614  ovnhoilem1  45615  hoi2toco  45621  ovncvr2  45625  hspdifhsp  45630  voncmpl  45635  hoiqssbl  45639  hspmbllem2  45641  hspmbl  45643  hoimbllem  45644  opnvonmbllem2  45647  mblvon  45653  ovolval3  45661  ovolval4lem1  45663  ovnovollem1  45670  ovnovollem2  45671  vonsn  45705  issmflem  45741  sssmf  45752  issmflelem  45758  issmfgtlem  45769  issmfgt  45770  smfaddlem1  45777  issmfgelem  45783  smflimlem3  45787  smfmullem2  45806  smfmullem4  45808  smfsuplem1  45825  smfsupmpt  45829  smfinfmpt  45833  smflimsuplem2  45835  smflimsuplem4  45837  smflimsupmpt  45843  smfliminfmpt  45846  fsupdm  45856  finfdm  45860  fzoopth  46333  zlmodzxzel  47119  ply1mulgsum  47158  catprs  47718  thincmod  47738  mndtcob  47795  mndtccatid  47800  mndtcid  47802  grptcmon  47803  grptcepi  47804