Theorem eleqtrd 2885

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

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-clel 2863

This theorem is referenced by:  eleqtrrd  2886  syl5eleq  2889  syl6eleq  2893  3eltr3d  2897  prel12g  4701  opth1  5259  0nelop  5277  fvelimad  6600  fviss  6608  tfisi  7429  fnwelem  7678  wfrlem17  7823  omeulem1  8058  oeeulem  8077  oeeui  8078  oaabs2  8122  omabs  8124  ercl  8150  erth  8188  ecelqsdm  8217  ordtypelem6  8833  ordtypelem7  8834  cantnfval  8977  cantnfp1lem3  8989  cantnflem4  9001  r1pwss  9059  rankonidlem  9103  rankxplim3  9156  fseqenlem2  9297  iunfictbso  9386  dfac12lem1  9415  dfac12lem2  9416  fin23lem30  9610  iundom2g  9808  fpwwe2lem6  9903  fpwwe2lem9  9906  lincmb01cmp  12731  fzopth  12794  fzoaddel2  12943  fzosubel2  12947  fzocatel  12951  zpnn0elfzo1  12961  fzoend  12978  peano2fzor  12994  monoord2  13251  sermono  13252  expmulnbnd  13446  bcpasc  13531  swrdcl  13843  revcl  13959  revlen  13960  fsum0diag2  14971  isumsplit  15028  fprodser  15136  sadadd  15649  sadass  15653  smuval2  15664  smumul  15675  vdwapun  16139  vdwlem9  16154  ramub1lem1  16191  prdsbasfn  16573  prdsbasprj  16574  pwsplusgval  16592  pwsmulrval  16593  pwsvscafval  16596  xpsaddlem  16675  xpsvsca  16679  xpsle  16681  mreexmrid  16743  homfeqval  16796  comfval2  16802  comfeq  16805  comfeqval  16807  oppccomfpropd  16826  invco  16870  sectepi  16883  issubc3  16948  funcf2  16967  fthepi  17027  nat1st2nd  17050  homarcl2  17124  coapm  17160  setcmon  17176  setcepi  17177  setcsect  17178  setcinv  17179  setciso  17180  catccatid  17191  resscatc  17194  catciso  17196  catcoppccl  17197  catcfuccl  17198  xpccatid  17267  catcxpccl  17286  xpcpropd  17287  evlfcl  17301  curfpropd  17312  hofcl  17338  yonedalem3  17359  yonffthlem  17361  poslubdg  17588  grpidd  17707  gsumress  17715  ismndd  17752  mndpropd  17755  issubmnd  17757  submnd0  17759  imasmnd  17767  frmdelbas  17829  grpidd2  17898  pwsinvg  17969  imasgrp  17972  submmulg  18025  subginvcl  18042  subgcl  18043  subgsub  18045  subgmulg  18047  quseccl  18089  gaid2  18174  submod  18424  odsubdvds  18426  sylow1lem4  18456  sylow2alem2  18473  lsmdisj2  18535  subgdisj1  18544  pj1id  18552  efgsrel  18587  efgrelexlemb  18603  efgcpbl2  18610  frgpcpbl  18612  frgp0  18613  frgpeccl  18614  frgpadd  18616  frgpup3lem  18630  frgpnabllem1  18716  cycsubgcyg  18742  prdsgsum  18818  dprdfeq0  18861  dmdprdsplitlem  18876  dpjidcl  18897  pgpfac1lem3a  18915  pgpfac1lem4  18917  pgpfaclem1  18920  pgpfaclem2  18921  ablfaclem2  18925  ringidss  19017  ringpropd  19022  imasring  19059  qusring2  19060  kerf1ghm  19187  kerf1hrmOLD  19188  subrg1  19235  subrgmcl  19237  subrgdv  19242  subrgunit  19243  issubdrg  19250  resrhm  19254  lmodprop2d  19386  0lmhm  19502  lmhmpropd  19535  lspfixed  19590  lssacsex  19606  lbsextlem4  19623  quscrng  19702  assapropd  19789  psrelbas  19847  resspsrvsca  19886  subrgpsr  19887  mplcoe1  19933  mplbas2  19938  mplascl  19963  mplmon2cl  19967  mplmon2mul  19968  evlrhm  19992  mpfconst  19997  mhpvscacl  20024  vr1cl2  20044  ply1lss  20047  ply1subrg  20048  psropprmul  20089  evl1vsd  20189  evl1expd  20190  evl1gsumadd  20203  evl1gsummon  20210  znf1o  20380  psgnghm2  20407  elocv  20494  pjff  20538  frlmlss  20577  frlmsubgval  20591  frlmvscafval  20592  frlmvscavalb  20596  frlmvplusgscavalb  20597  frlmphl  20607  uvcresum  20619  frlmssuvc1  20620  frlmssuvc2  20621  frlmsslsp  20622  frlmup1  20624  matring  20736  matassa  20737  mat1  20740  mattposcl  20746  mavmulass  20842  mdetunilem9  20913  matinv  20970  cpmadugsumlemF  21168  cpmadugsumfi  21169  cpmidgsum2  21171  elcls3  21375  mreclatdemoBAD  21388  neiptopnei  21424  resstps  21479  ordtrest2lem  21495  ordtrest2  21496  pnfnei  21512  mnfnei  21513  iscnp2  21531  iscnp4  21555  cnrest2r  21579  lmcls  21594  lmcld  21595  cnt0  21638  cnhaus  21646  isreg2  21669  connclo  21707  1stccnp  21754  loclly  21779  lly1stc  21788  locfincmp  21818  unisngl  21819  comppfsc  21824  kgencmp2  21838  llycmpkgen2  21842  kgen2ss  21847  kgencn3  21850  pttoponconst  21889  txcls  21896  txbasval  21898  dfac14lem  21909  ptcn  21919  ptrescn  21931  txtube  21932  txcmplem1  21933  txlm  21940  txkgen  21944  xkopjcn  21948  cnmptkp  21972  xkoinjcn  21979  qtopkgen  22002  imastps  22013  isr0  22029  r0cld  22030  pt1hmeo  22098  ptuncnv  22099  ptunhmeo  22100  filintn0  22153  trnei  22184  flimfil  22261  flimopn  22267  fbflim2  22269  cnpflf2  22292  flfcnp  22296  flfcnp2  22299  fclsopn  22306  fcfnei  22327  cnpfcf  22333  flfcntr  22335  alexsublem  22336  ptcmplem3  22346  ptcmplem4  22347  cnextfres1  22360  tmdcn2  22381  tmdgsum  22387  tmdgsum2  22388  symgtgp  22393  tgphaus  22408  tgpt1  22409  qustgplem  22412  prdstmdd  22415  prdstgpd  22416  haustsms  22427  tsmscls  22429  tsmsmhm  22437  tsmsadd  22438  tgptsmscls  22441  tsmssplit  22443  restutop  22529  utopreg  22544  ressusp  22557  ucncn  22577  xmetunirn  22630  ressprdsds  22664  xpsdsval  22674  xblss2ps  22694  blbas  22723  mopntopon  22732  isxms2  22741  imasf1oxms  22782  imasf1oms  22783  prdsxmslem2  22822  tmsxpsval  22831  tngngp2  22944  tngngp  22946  tgioo  23087  metdseq0  23145  cncfmpt2f  23205  cncfcnvcn  23212  cnmptre  23214  cnheibor  23242  nmhmcn  23407  cvsdiv  23419  cvsdivcl  23420  cphsubrglem  23464  cphreccllem  23465  iscmet3  23579  relcmpcmet  23604  bcthlem4  23613  rrxds  23679  rrxvsca  23680  rrxplusgvscavalb  23681  rrxbasefi  23696  rrxmetfi  23698  minveclem4  23718  ivthicc  23742  evthicc  23743  ovolicc2lem4  23804  ovolicc2lem5  23805  iunmbl2  23841  vitalilem3  23894  cncombf  23942  cnmbf  23943  dvres2lem  24191  cpncn  24216  cpnres  24217  dvaddbr  24218  dvmulbr  24219  dvcobr  24226  dvcjbr  24229  dvrec  24235  dvcnvlem  24256  dvlip2  24275  dvivth  24290  lhop2  24295  lhop  24296  dvcnvrelem1  24297  dvcnvrelem2  24298  dvcnvre  24299  ftc1lem6  24321  mdegvscale  24352  mdegvsca  24353  fta1blem  24445  plyaddlem1  24486  plymullem1  24487  coeeulem  24497  tayl0  24633  taylthlem1  24644  taylthlem2  24645  ulmdvlem3  24673  psercnlem2  24695  psercn  24697  efsubm  24816  cxpcn3  25010  loglesqrt  25020  efrlim  25229  ppinprm  25411  chtnprm  25413  dchrptlem1  25522  dchrptlem2  25523  tgbtwnouttr2  25963  tgldim0eq  25971  tgifscgr  25976  iscgrglt  25982  ercgrg  25985  tgcgrxfr  25986  motcgrg  26012  tglngne  26018  tgcolg  26022  tgbtwnconn1lem2  26041  tgbtwnconn1lem3  26042  legtri3  26058  legbtwn  26062  ncolne1  26093  tgisline  26095  tglinethru  26104  coltr3  26116  colline  26117  tglowdim2ln  26119  mirinv  26134  miriso  26138  mirauto  26152  miduniq  26153  krippenlem  26158  midexlem  26160  ragperp  26185  footexALT  26186  footexlem2  26188  perpdragALT  26195  perpdrag  26196  colperpexlem1  26198  colperpexlem3  26200  mideulem2  26202  midex  26205  opphllem1  26215  opphllem3  26217  opphllem4  26218  hlpasch  26224  trgcopy  26272  f1otrg  26340  axlowdimlem16  26426  elntg  26453  eengtrkg  26455  eengtrkge  26456  grpoidinv2  27983  grpoinv  27993  ubthlem2  28339  shuni  28768  acunirnmpt  30094  acunirnmpt2  30095  acunirnmpt2f  30096  fpwrelmap  30157  odpmco  30389  pmtrcnel  30392  pmtrcnel2  30393  pmtrcnelor  30394  tocyc01  30407  trsp2cyc  30412  cycpmconjv  30421  cycpmrn  30422  tocyccntz  30423  gsummpt2d  30496  rngurd  30511  freshmansdream  30513  srasubrg  30593  drgextlsp  30600  matdim  30617  lbslsat  30618  lindsunlem  30624  lbsdiflsp0  30626  dimkerim  30627  fedgmullem1  30629  fedgmullem2  30630  fedgmul  30631  fldexttr  30652  extdgmul  30655  extdg1id  30657  ordtrest2NEWlem  30782  ordtrest2NEW  30783  lmxrge0  30812  nmmulg  30826  rrhcn  30855  esumadd  30933  esumaddf  30937  esumcocn  30956  measiuns  31093  mbfmco2  31140  dya2iocnrect  31156  omscl  31170  omsf  31171  oms0  31172  sibf0  31209  sibfof  31215  sitgaddlemb  31223  fibp1  31276  ccatmulgnn0dir  31429  cxpcncf1  31483  ftc2re  31486  fsum2dsub  31495  reprf  31500  reprsum  31501  bnj1450  31936  bnj1501  31953  indispconn  32090  connpconn  32091  pconnpi1  32093  sconnpi1  32095  cvmsss2  32130  cvmliftmolem1  32137  cvmliftlem8  32148  cvmliftlem10  32150  cvmliftlem11  32151  cvmlift2lem9  32167  cvmlift2lem12  32170  cvmlift3lem7  32181  mrsubcv  32366  mrsubff  32368  mrsubccat  32374  elmrsubrn  32376  mrsubco  32377  mrsubvrs  32378  frrlem8  32740  frrlem10  32742  nodenselem5  32802  linethru  33224  ivthALT  33293  neibastop2  33319  filnetlem4  33339  matunitlindflem2  34439  poimirlem1  34443  poimirlem2  34444  poimirlem8  34450  poimirlem9  34451  poimirlem16  34458  poimirlem17  34459  poimirlem19  34461  poimirlem20  34462  poimirlem22  34464  poimirlem23  34465  poimir  34475  broucube  34476  areacirclem4  34535  fdc  34571  isbnd3  34613  prdsbnd  34622  prdstotbnd  34623  prdsbnd2  34624  rrnequiv  34664  reheibor  34668  iscringd  34827  isfldidl  34897  eqvrelth  35396  eqlkr  35785  ldualvsubval  35843  dvalveclem  37711  dia2dimlem5  37754  dia2dimlem9  37758  tendoinvcl  37790  dvhgrp  37793  dvhlveclem  37794  dihpN  38022  dochsnkr2cl  38160  lcfl7lem  38185  lclkr  38219  lclkrs  38225  lcfrvalsnN  38227  lcfrlem4  38231  lcfrlem6  38233  lcfrlem16  38244  lcdvsubval  38304  lcdlkreqN  38308  mapdcl2  38342  mapdincl  38347  mapdlsmcl  38349  mapdpglem3  38361  hdmaprnlem9N  38543  hdmaplkr  38599  hdmapip0  38601  hdmapglem7a  38613  fltnltalem  38790  diophin  38873  acongeq  39084  isnumbasgrplem2  39208  proot1mul  39303  iunrelexpuztr  39568  ntrclsiex  39907  ntrneiiex  39930  ntrneinex  39931  elnelneqd  40060  hash1elsn  40076  grurankcld  40085  1nsgtrivd  40158  simpgnsgeqd  40176  simpgnsgbid  40178  ablsimpnosubgd  40181  bccbc  40234  suctrALT  40718  restuni3  40943  disjf1o  41011  disjinfi  41013  choicefi  41022  fsneq  41028  fsneqrn  41033  unirnmapsn  41036  iunmapsn  41039  monoords  41124  elfzolem1  41149  uzfissfz  41154  monoord2xrv  41321  evthiccabs  41332  iooabslt  41335  tgqioo2  41384  islptre  41461  limciccioolb  41463  sumnnodd  41472  limcicciooub  41479  lptre2pt  41482  limcresiooub  41484  limcresioolb  41485  lptioo1cn  41488  reclimc  41495  liminfvalxr  41625  liminfvaluz  41634  limsupvaluz3  41640  fsumcncf  41722  ioccncflimc  41729  cncfuni  41730  icccncfext  41731  cncficcgt0  41732  icocncflimc  41733  cncfdmsn  41734  cncfiooicclem1  41737  cncfiooicc  41738  cncfioobd  41741  cxpcncf2  41744  fprodsub2cncf  41750  fprodadd2cncf  41751  fperdvper  41764  dvcosax  41772  dvnmul  41789  dvnprodlem1  41792  dvnprodlem2  41793  itgsubsticclem  41821  fvvolioof  41836  fvvolicof  41838  stoweidlem26  41873  stoweidlem27  41874  stoweidlem31  41878  stoweidlem34  41881  dirkercncflem2  41951  dirkercncflem3  41952  dirkercncflem4  41953  dirkercncf  41954  fourierdlem16  41970  fourierdlem20  41974  fourierdlem21  41975  fourierdlem22  41976  fourierdlem26  41980  fourierdlem32  41986  fourierdlem33  41987  fourierdlem38  41992  fourierdlem39  41993  fourierdlem46  41999  fourierdlem48  42001  fourierdlem49  42002  fourierdlem53  42006  fourierdlem60  42013  fourierdlem61  42014  fourierdlem69  42022  fourierdlem70  42023  fourierdlem71  42024  fourierdlem73  42026  fourierdlem74  42027  fourierdlem75  42028  fourierdlem76  42029  fourierdlem80  42033  fourierdlem81  42034  fourierdlem82  42035  fourierdlem83  42036  fourierdlem84  42037  fourierdlem85  42038  fourierdlem88  42041  fourierdlem89  42042  fourierdlem91  42044  fourierdlem92  42045  fourierdlem93  42046  fourierdlem100  42053  fourierdlem101  42054  fourierdlem103  42056  fourierdlem104  42057  fourierdlem107  42060  fourierdlem111  42064  fourierdlem112  42065  fourierdlem113  42066  fouriersw  42078  fouriercn  42079  etransclem24  42105  etransclem26  42107  etransclem28  42109  etransclem31  42112  etransclem32  42113  etransclem33  42114  etransclem34  42115  etransclem35  42116  etransclem38  42119  rrxtopnfi  42134  rrxtoponfi  42138  qndenserrnbl  42142  qndenserrnopnlem  42144  qndenserrn  42146  rrnprjdstle  42148  ioorrnopnlem  42151  prsal  42165  intsaluni  42174  salgencntex  42188  subsaliuncllem  42202  fge0iccico  42214  sge0sn  42223  sge0tsms  42224  sge0cl  42225  sge0f1o  42226  sge0pr  42238  sge0isum  42271  nnfoctbdjlem  42299  iundjiunlem  42303  iundjiun  42304  meadjiunlem  42309  psmeasure  42315  meaiininclem  42330  caragenelss  42345  omeunile  42349  carageniuncllem1  42365  carageniuncllem2  42366  0ome  42373  isomenndlem  42374  isomennd  42375  hoicvr  42392  ovnpnfelsup  42403  ovncvrrp  42408  ovnsubaddlem1  42414  hoidmv1le  42438  hoidmvlelem2  42440  hoidmvlelem3  42441  hoidmvlelem4  42442  hoidmvle  42444  ovnhoilem1  42445  hoi2toco  42451  ovncvr2  42455  hspdifhsp  42460  voncmpl  42465  hoiqssbl  42469  hspmbllem2  42471  hspmbl  42473  hoimbllem  42474  opnvonmbllem2  42477  mblvon  42483  ovolval3  42491  ovolval4lem1  42493  ovnovollem1  42500  ovnovollem2  42501  vonsn  42535  issmflem  42566  sssmf  42577  issmflelem  42583  issmfgtlem  42594  issmfgt  42595  smfaddlem1  42601  issmfgelem  42607  smflimlem3  42611  smfmullem2  42629  smfmullem4  42631  smfsuplem1  42647  smfsupmpt  42651  smfinfmpt  42655  smflimsuplem2  42657  smflimsuplem4  42659  smflimsupmpt  42665  smfliminfmpt  42668  fzoopth  43063  issubmgm2  43559  zlmodzxzel  43901  ply1mulgsum  43944