Theorem eleqtrd 2842

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

Syntax hints:   → wi 4   = wceq 1539   ∈ 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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  eleqtrrd  2843  eleqtrid  2846  eleqtrdi  2850  3eltr3d  2854  prel12g  4795  opth1  5391  0nelop  5411  fvelimad  6845  fviss  6854  tfisi  7714  fnwelem  7981  frrlem8  8118  frrlem10  8120  fprresex  8135  wfrlem17OLD  8165  omeulem1  8422  oeeulem  8441  oeeui  8442  oaabs2  8488  omabs  8490  ercl  8518  erth  8556  ecelqsdm  8585  ordtypelem6  9291  ordtypelem7  9292  cantnfval  9435  cantnfp1lem3  9447  cantnflem4  9459  r1pwss  9551  rankonidlem  9595  rankxplim3  9648  fseqenlem2  9790  iunfictbso  9879  dfac12lem1  9908  dfac12lem2  9909  fin23lem30  10107  iundom2g  10305  fpwwe2lem5  10400  fpwwe2lem8  10403  lincmb01cmp  13236  fzopth  13302  fzoaddel2  13452  fzosubel2  13456  fzocatel  13460  zpnn0elfzo1  13470  fzoend  13487  peano2fzor  13503  monoord2  13763  sermono  13764  expmulnbnd  13959  bcpasc  14044  hash1elsn  14095  swrdcl  14367  revcl  14483  revlen  14484  fsum0diag2  15504  isumsplit  15561  fprodser  15668  sadadd  16183  sadass  16187  smuval2  16198  smumul  16209  vdwapun  16684  vdwlem9  16699  ramub1lem1  16736  prdsbasfn  17191  prdsbasprj  17192  pwsplusgval  17210  pwsmulrval  17211  pwsvscafval  17214  xpsaddlem  17293  xpsvsca  17297  xpsle  17299  mreexmrid  17361  homfeqval  17415  comfval2  17421  comfeq  17424  comfeqval  17426  oppccomfpropd  17447  invco  17492  sectepi  17505  issubc3  17573  funcf2  17592  fthepi  17653  nat1st2nd  17676  homarcl2  17759  coapm  17795  setcmon  17811  setcepi  17812  setcsect  17813  setcinv  17814  setciso  17815  cat1lem  17820  catccatid  17830  resscatc  17833  catciso  17835  catcbascl  17836  catcoppccl  17841  catcoppcclOLD  17842  catcfuccl  17843  catcfucclOLD  17844  xpccatid  17914  catcxpccl  17933  catcxpcclOLD  17934  xpcpropd  17935  evlfcl  17949  curfpropd  17960  hofcl  17986  yonedalem3  18007  yonffthlem  18009  poslubdg  18141  grpidd  18364  gsumress  18375  ismndd  18416  mndpropd  18419  issubmnd  18421  submnd0  18423  imasmnd  18432  frmdelbas  18501  grpidd2  18626  pwsinvg  18697  imasgrp  18700  submmulg  18756  subginvcl  18773  subgcl  18774  subgsub  18776  subgmulg  18778  1nsgtrivd  18811  quseccl  18821  gaid2  18918  submod  19183  odsubdvds  19185  sylow1lem4  19215  sylow2alem2  19232  lsmdisj2  19297  subgdisj1  19306  pj1id  19314  efgsrel  19349  efgrelexlemb  19365  efgcpbl2  19372  frgpcpbl  19374  frgp0  19375  frgpeccl  19376  frgpadd  19378  frgpup3lem  19392  frgpnabllem1  19483  cycsubgcyg  19511  prdsgsum  19591  dprdfeq0  19634  dmdprdsplitlem  19649  dpjidcl  19670  pgpfac1lem3a  19688  pgpfac1lem4  19690  pgpfaclem1  19693  pgpfaclem2  19694  ablfaclem2  19698  simpgnsgeqd  19713  simpgnsgbid  19715  ablsimpnosubgd  19716  ringidss  19825  ringpropd  19830  imasring  19867  qusring2  19868  kerf1ghm  19996  subrg1  20043  subrgmcl  20045  subrgdv  20050  subrgunit  20051  issubdrg  20058  resrhm  20062  lmodprop2d  20194  0lmhm  20311  lmhmpropd  20344  lspfixed  20399  lssacsex  20415  lbsextlem4  20432  quscrng  20520  znf1o  20768  psgnghm2  20795  elocv  20882  pjff  20928  frlmlss  20967  frlmsubgval  20981  frlmvscafval  20982  frlmvscavalb  20986  frlmvplusgscavalb  20987  frlmphl  20997  uvcresum  21009  frlmssuvc1  21010  frlmssuvc2  21011  frlmsslsp  21012  frlmup1  21014  assapropd  21085  psrelbas  21157  resspsrvsca  21196  subrgpsr  21197  mplcoe1  21247  mplbas2  21252  mplascl  21281  mplmon2cl  21285  mplmon2mul  21286  evlrhm  21315  mpfconst  21320  mhpvscacl  21353  vr1cl2  21373  ply1lss  21376  ply1subrg  21377  psropprmul  21418  evl1vsd  21519  evl1expd  21520  evl1gsumadd  21533  evl1gsummon  21540  matring  21601  matassa  21602  mat1  21605  mattposcl  21611  mavmulass  21707  mdetunilem9  21778  matinv  21835  cpmadugsumlemF  22034  cpmadugsumfi  22035  cpmidgsum2  22037  elcls3  22243  mreclatdemoBAD  22256  neiptopnei  22292  resstps  22347  ordtrest2lem  22363  ordtrest2  22364  pnfnei  22380  mnfnei  22381  iscnp2  22399  iscnp4  22423  cnrest2r  22447  lmcls  22462  lmcld  22463  cnt0  22506  cnhaus  22514  isreg2  22537  connclo  22575  1stccnp  22622  loclly  22647  lly1stc  22656  locfincmp  22686  unisngl  22687  comppfsc  22692  kgencmp2  22706  llycmpkgen2  22710  kgen2ss  22715  kgencn3  22718  pttoponconst  22757  txcls  22764  txbasval  22766  dfac14lem  22777  ptcn  22787  ptrescn  22799  txtube  22800  txcmplem1  22801  txlm  22808  txkgen  22812  xkopjcn  22816  cnmptkp  22840  xkoinjcn  22847  qtopkgen  22870  imastps  22881  isr0  22897  r0cld  22898  pt1hmeo  22966  ptuncnv  22967  ptunhmeo  22968  filintn0  23021  trnei  23052  flimfil  23129  flimopn  23135  fbflim2  23137  cnpflf2  23160  flfcnp  23164  flfcnp2  23167  fclsopn  23174  fcfnei  23195  cnpfcf  23201  flfcntr  23203  alexsublem  23204  ptcmplem3  23214  ptcmplem4  23215  cnextfres1  23228  tmdcn2  23249  tmdgsum  23255  tmdgsum2  23256  efmndtmd  23261  symgtgp  23266  tgphaus  23277  tgpt1  23278  qustgplem  23281  prdstmdd  23284  prdstgpd  23285  haustsms  23296  tsmscls  23298  tsmsmhm  23306  tsmsadd  23307  tgptsmscls  23310  tsmssplit  23312  restutop  23398  utopreg  23413  ressusp  23425  ucncn  23446  xmetunirn  23499  ressprdsds  23533  xpsdsval  23543  xblss2ps  23563  blbas  23592  mopntopon  23601  isxms2  23610  imasf1oxms  23654  imasf1oms  23655  prdsxmslem2  23694  tmsxpsval  23703  tngngp2  23825  tngngp  23827  tgioo  23968  metdseq0  24026  cncfmpt2f  24087  cncfcnvcn  24097  cnmptre  24099  cnheibor  24127  nmhmcn  24292  cvsdiv  24304  cvsdivcl  24305  cphsubrglem  24350  cphreccllem  24351  iscmet3  24466  relcmpcmet  24491  bcthlem4  24500  rrxds  24566  rrxvsca  24567  rrxplusgvscavalb  24568  rrxbasefi  24583  rrxmetfi  24585  minveclem4  24605  ivthicc  24631  evthicc  24632  ovolicc2lem4  24693  ovolicc2lem5  24694  iunmbl2  24730  vitalilem3  24783  cncombf  24831  cnmbf  24832  dvres2lem  25083  cpncn  25109  cpnres  25110  dvaddbr  25111  dvmulbr  25112  dvcobr  25119  dvcjbr  25122  dvrec  25128  dvcnvlem  25149  dvlip2  25168  dvivth  25183  lhop2  25188  lhop  25189  dvcnvrelem1  25190  dvcnvrelem2  25191  dvcnvre  25192  ftc1lem6  25214  mdegvscale  25249  mdegvsca  25250  fta1blem  25342  plyaddlem1  25383  plymullem1  25384  coeeulem  25394  tayl0  25530  taylthlem1  25541  taylthlem2  25542  ulmdvlem3  25570  psercnlem2  25592  psercn  25594  efsubm  25716  cxpcn3  25910  loglesqrt  25920  efrlim  26128  ppinprm  26310  chtnprm  26312  dchrptlem1  26421  dchrptlem2  26422  tgbtwnouttr2  26865  tgldim0eq  26873  tgifscgr  26878  iscgrglt  26884  ercgrg  26887  tgcgrxfr  26888  motcgrg  26914  tglngne  26920  tgcolg  26924  tgbtwnconn1lem2  26943  tgbtwnconn1lem3  26944  legtri3  26960  legbtwn  26964  ncolne1  26995  tgisline  26997  tglinethru  27006  coltr3  27018  colline  27019  tglowdim2ln  27021  mirinv  27036  miriso  27040  mirauto  27054  miduniq  27055  krippenlem  27060  midexlem  27062  ragperp  27087  footexALT  27088  footexlem2  27090  perpdragALT  27097  perpdrag  27098  colperpexlem1  27100  colperpexlem3  27102  mideulem2  27104  midex  27107  opphllem1  27117  opphllem3  27119  opphllem4  27120  hlpasch  27126  trgcopy  27174  f1otrg  27241  axlowdimlem16  27334  elntg  27361  eengtrkg  27363  eengtrkge  27364  clwwlkccatlem  28362  grpoidinv2  28886  grpoinv  28896  ubthlem2  29242  shuni  29671  acunirnmpt  31005  acunirnmpt2  31006  acunirnmpt2f  31007  fpwrelmap  31077  fzm1ne1  31119  fzom1ne1  31131  ccatf1  31232  swrdf1  31237  gsummpt2d  31318  gsumhashmul  31325  odpmco  31364  pmtrcnel  31367  pmtrcnel2  31368  pmtrcnelor  31369  tocyc01  31394  trsp2cyc  31399  cycpmco2f1  31400  cycpmco2rn  31401  cycpmco2lem1  31402  cycpmco2lem2  31403  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmco2  31409  cycpmconjv  31418  cycpmrn  31419  tocyccntz  31420  rngurd  31491  freshmansdream  31493  pidlnz  31580  nsgmgc  31606  elrspunidl  31615  qsidomlem1  31637  idlsrg0g  31660  ply1chr  31678  srasubrg  31683  drgextlsp  31690  matdim  31707  lbslsat  31708  lindsunlem  31714  lbsdiflsp0  31716  dimkerim  31717  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  fldexttr  31742  extdgmul  31745  extdg1id  31747  rspectopn  31826  zarclsiin  31830  zarmxt1  31839  rspectps  31842  rhmpreimacn  31844  ordtrest2NEWlem  31881  ordtrest2NEW  31882  lmxrge0  31911  nmmulg  31927  rrhcn  31956  esumadd  32034  esumaddf  32038  esumcocn  32057  measiuns  32194  mbfmco2  32241  dya2iocnrect  32257  omscl  32271  omsf  32272  oms0  32273  sibf0  32310  sibfof  32316  sitgaddlemb  32324  fibp1  32377  ccatmulgnn0dir  32530  cxpcncf1  32584  ftc2re  32587  fsum2dsub  32596  reprf  32601  reprsum  32602  bnj1450  33039  bnj1501  33056  revpfxsfxrev  33086  indispconn  33205  connpconn  33206  pconnpi1  33208  sconnpi1  33210  cvmsss2  33245  cvmliftmolem1  33252  cvmliftlem8  33263  cvmliftlem10  33265  cvmliftlem11  33266  cvmlift2lem9  33282  cvmlift2lem12  33285  cvmlift3lem7  33296  mrsubcv  33481  mrsubff  33483  mrsubccat  33489  elmrsubrn  33491  mrsubco  33492  mrsubvrs  33493  nodenselem5  33900  oldlim  34078  cofcutr  34101  linethru  34464  ivthALT  34533  neibastop2  34559  filnetlem4  34579  matunitlindflem2  35783  poimirlem1  35787  poimirlem2  35788  poimirlem8  35794  poimirlem9  35795  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimir  35819  broucube  35820  areacirclem4  35877  fdc  35912  isbnd3  35951  prdsbnd  35960  prdstotbnd  35961  prdsbnd2  35962  rrnequiv  36002  reheibor  36006  iscringd  36165  isfldidl  36235  eqvrelth  36731  eqlkr  37120  ldualvsubval  37178  dvalveclem  39046  dia2dimlem5  39089  dia2dimlem9  39093  tendoinvcl  39125  dvhgrp  39128  dvhlveclem  39129  dihpN  39357  dochsnkr2cl  39495  lcfl7lem  39520  lclkr  39554  lclkrs  39560  lcfrvalsnN  39562  lcfrlem4  39566  lcfrlem6  39568  lcfrlem16  39579  lcdvsubval  39639  lcdlkreqN  39643  mapdcl2  39677  mapdincl  39682  mapdlsmcl  39684  mapdpglem3  39696  hdmaprnlem9N  39878  hdmaplkr  39934  hdmapip0  39936  hdmapglem7a  39948  sticksstones11  40119  sticksstones12a  40120  sticksstones19  40128  evlsscaval  40280  mhphf  40292  mhphf2  40293  mhphf4  40295  prjspnvs  40466  prjspner1  40470  prjcrv0  40477  fltnltalem  40506  diophin  40601  acongeq  40812  isnumbasgrplem2  40936  proot1mul  41031  iunrelexpuztr  41334  ntrclsiex  41670  ntrneiiex  41693  ntrneinex  41694  elnelneqd  41820  grurankcld  41858  bccbc  41970  suctrALT  42453  restuni3  42674  disjf1o  42736  disjinfi  42738  choicefi  42747  fsneq  42753  fsneqrn  42758  unirnmapsn  42761  iunmapsn  42764  monoords  42843  elfzolem1  42867  uzfissfz  42872  monoord2xrv  43031  evthiccabs  43041  iooabslt  43044  tgqioo2  43092  islptre  43167  limciccioolb  43169  sumnnodd  43178  limcicciooub  43185  lptre2pt  43188  limcresiooub  43190  limcresioolb  43191  lptioo1cn  43194  reclimc  43201  liminfvalxr  43331  liminfvaluz  43340  limsupvaluz3  43346  fsumcncf  43426  ioccncflimc  43433  cncfuni  43434  icccncfext  43435  cncficcgt0  43436  icocncflimc  43437  cncfdmsn  43438  cncfiooicclem1  43441  cncfiooicc  43442  cncfioobd  43445  cxpcncf2  43447  fprodsub2cncf  43453  fprodadd2cncf  43454  fperdvper  43467  dvcosax  43474  dvnmul  43491  dvnprodlem1  43494  dvnprodlem2  43495  itgsubsticclem  43523  fvvolioof  43537  fvvolicof  43539  stoweidlem26  43574  stoweidlem27  43575  stoweidlem31  43579  stoweidlem34  43582  dirkercncflem2  43652  dirkercncflem3  43653  dirkercncflem4  43654  dirkercncf  43655  fourierdlem16  43671  fourierdlem20  43675  fourierdlem21  43676  fourierdlem22  43677  fourierdlem26  43681  fourierdlem32  43687  fourierdlem33  43688  fourierdlem38  43693  fourierdlem39  43694  fourierdlem46  43700  fourierdlem48  43702  fourierdlem49  43703  fourierdlem53  43707  fourierdlem60  43714  fourierdlem61  43715  fourierdlem69  43723  fourierdlem70  43724  fourierdlem71  43725  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem80  43734  fourierdlem81  43735  fourierdlem82  43736  fourierdlem83  43737  fourierdlem84  43738  fourierdlem85  43739  fourierdlem88  43742  fourierdlem89  43743  fourierdlem91  43745  fourierdlem92  43746  fourierdlem93  43747  fourierdlem100  43754  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fouriersw  43779  fouriercn  43780  etransclem24  43806  etransclem26  43808  etransclem28  43810  etransclem31  43813  etransclem32  43814  etransclem33  43815  etransclem34  43816  etransclem35  43817  etransclem38  43820  rrxtopnfi  43835  rrxtoponfi  43839  qndenserrnbl  43843  qndenserrnopnlem  43845  qndenserrn  43847  rrnprjdstle  43849  ioorrnopnlem  43852  prsal  43866  intsaluni  43875  salgencntex  43889  subsaliuncllem  43903  fge0iccico  43915  sge0sn  43924  sge0tsms  43925  sge0cl  43926  sge0f1o  43927  sge0pr  43939  sge0isum  43972  nnfoctbdjlem  44000  iundjiunlem  44004  iundjiun  44005  meadjiunlem  44010  psmeasure  44016  meaiininclem  44031  caragenelss  44046  omeunile  44050  carageniuncllem1  44066  carageniuncllem2  44067  0ome  44074  isomenndlem  44075  isomennd  44076  hoicvr  44093  ovnpnfelsup  44104  ovncvrrp  44109  ovnsubaddlem1  44115  hoidmv1le  44139  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  hoidmvle  44145  ovnhoilem1  44146  hoi2toco  44152  ovncvr2  44156  hspdifhsp  44161  voncmpl  44166  hoiqssbl  44170  hspmbllem2  44172  hspmbl  44174  hoimbllem  44175  opnvonmbllem2  44178  mblvon  44184  ovolval3  44192  ovolval4lem1  44194  ovnovollem1  44201  ovnovollem2  44202  vonsn  44236  issmflem  44272  sssmf  44283  issmflelem  44289  issmfgtlem  44300  issmfgt  44301  smfaddlem1  44308  issmfgelem  44314  smflimlem3  44318  smfmullem2  44337  smfmullem4  44339  smfsuplem1  44355  smfsupmpt  44359  smfinfmpt  44363  smflimsuplem2  44365  smflimsuplem4  44367  smflimsupmpt  44373  smfliminfmpt  44376  fzoopth  44830  issubmgm2  45355  zlmodzxzel  45702  ply1mulgsum  45742  catprs  46303  thincmod  46323  mndtcob  46380  mndtccatid  46385  mndtcid  46387  grptcmon  46388  grptcepi  46389