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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809

This theorem is referenced by:  eleqtrrd  2834  eleqtrid  2837  eleqtrdi  2841  3eltr3d  2845  prel12g  4760  opth1  5344  0nelop  5364  fvelimad  6757  fviss  6766  tfisi  7615  fnwelem  7876  frrlem8  8012  frrlem10  8014  wfrlem17  8049  omeulem1  8288  oeeulem  8307  oeeui  8308  oaabs2  8352  omabs  8354  ercl  8380  erth  8418  ecelqsdm  8447  ordtypelem6  9117  ordtypelem7  9118  cantnfval  9261  cantnfp1lem3  9273  cantnflem4  9285  r1pwss  9365  rankonidlem  9409  rankxplim3  9462  fseqenlem2  9604  iunfictbso  9693  dfac12lem1  9722  dfac12lem2  9723  fin23lem30  9921  iundom2g  10119  fpwwe2lem5  10214  fpwwe2lem8  10217  lincmb01cmp  13048  fzopth  13114  fzoaddel2  13263  fzosubel2  13267  fzocatel  13271  zpnn0elfzo1  13281  fzoend  13298  peano2fzor  13314  monoord2  13572  sermono  13573  expmulnbnd  13767  bcpasc  13852  hash1elsn  13903  swrdcl  14175  revcl  14291  revlen  14292  fsum0diag2  15310  isumsplit  15367  fprodser  15474  sadadd  15989  sadass  15993  smuval2  16004  smumul  16015  vdwapun  16490  vdwlem9  16505  ramub1lem1  16542  prdsbasfn  16930  prdsbasprj  16931  pwsplusgval  16949  pwsmulrval  16950  pwsvscafval  16953  xpsaddlem  17032  xpsvsca  17036  xpsle  17038  mreexmrid  17100  homfeqval  17154  comfval2  17160  comfeq  17163  comfeqval  17165  oppccomfpropd  17185  invco  17230  sectepi  17243  issubc3  17309  funcf2  17328  fthepi  17389  nat1st2nd  17412  homarcl2  17495  coapm  17531  setcmon  17547  setcepi  17548  setcsect  17549  setcinv  17550  setciso  17551  cat1lem  17556  catccatid  17566  resscatc  17569  catciso  17571  catcbascl  17572  catcoppccl  17577  catcoppcclOLD  17578  catcfuccl  17579  catcfucclOLD  17580  xpccatid  17649  catcxpccl  17668  catcxpcclOLD  17669  xpcpropd  17670  evlfcl  17684  curfpropd  17695  hofcl  17721  yonedalem3  17742  yonffthlem  17744  poslubdg  17874  grpidd  18097  gsumress  18108  ismndd  18149  mndpropd  18152  issubmnd  18154  submnd0  18156  imasmnd  18165  frmdelbas  18234  grpidd2  18359  pwsinvg  18430  imasgrp  18433  submmulg  18489  subginvcl  18506  subgcl  18507  subgsub  18509  subgmulg  18511  1nsgtrivd  18544  quseccl  18554  gaid2  18651  submod  18912  odsubdvds  18914  sylow1lem4  18944  sylow2alem2  18961  lsmdisj2  19026  subgdisj1  19035  pj1id  19043  efgsrel  19078  efgrelexlemb  19094  efgcpbl2  19101  frgpcpbl  19103  frgp0  19104  frgpeccl  19105  frgpadd  19107  frgpup3lem  19121  frgpnabllem1  19212  cycsubgcyg  19240  prdsgsum  19320  dprdfeq0  19363  dmdprdsplitlem  19378  dpjidcl  19399  pgpfac1lem3a  19417  pgpfac1lem4  19419  pgpfaclem1  19422  pgpfaclem2  19423  ablfaclem2  19427  simpgnsgeqd  19442  simpgnsgbid  19444  ablsimpnosubgd  19445  ringidss  19549  ringpropd  19554  imasring  19591  qusring2  19592  kerf1ghm  19717  subrg1  19764  subrgmcl  19766  subrgdv  19771  subrgunit  19772  issubdrg  19779  resrhm  19783  lmodprop2d  19915  0lmhm  20031  lmhmpropd  20064  lspfixed  20119  lssacsex  20135  lbsextlem4  20152  quscrng  20232  znf1o  20470  psgnghm2  20497  elocv  20584  pjff  20628  frlmlss  20667  frlmsubgval  20681  frlmvscafval  20682  frlmvscavalb  20686  frlmvplusgscavalb  20687  frlmphl  20697  uvcresum  20709  frlmssuvc1  20710  frlmssuvc2  20711  frlmsslsp  20712  frlmup1  20714  assapropd  20785  psrelbas  20858  resspsrvsca  20897  subrgpsr  20898  mplcoe1  20948  mplbas2  20953  mplascl  20976  mplmon2cl  20980  mplmon2mul  20981  evlrhm  21010  mpfconst  21015  mhpvscacl  21048  vr1cl2  21068  ply1lss  21071  ply1subrg  21072  psropprmul  21113  evl1vsd  21214  evl1expd  21215  evl1gsumadd  21228  evl1gsummon  21235  matring  21294  matassa  21295  mat1  21298  mattposcl  21304  mavmulass  21400  mdetunilem9  21471  matinv  21528  cpmadugsumlemF  21727  cpmadugsumfi  21728  cpmidgsum2  21730  elcls3  21934  mreclatdemoBAD  21947  neiptopnei  21983  resstps  22038  ordtrest2lem  22054  ordtrest2  22055  pnfnei  22071  mnfnei  22072  iscnp2  22090  iscnp4  22114  cnrest2r  22138  lmcls  22153  lmcld  22154  cnt0  22197  cnhaus  22205  isreg2  22228  connclo  22266  1stccnp  22313  loclly  22338  lly1stc  22347  locfincmp  22377  unisngl  22378  comppfsc  22383  kgencmp2  22397  llycmpkgen2  22401  kgen2ss  22406  kgencn3  22409  pttoponconst  22448  txcls  22455  txbasval  22457  dfac14lem  22468  ptcn  22478  ptrescn  22490  txtube  22491  txcmplem1  22492  txlm  22499  txkgen  22503  xkopjcn  22507  cnmptkp  22531  xkoinjcn  22538  qtopkgen  22561  imastps  22572  isr0  22588  r0cld  22589  pt1hmeo  22657  ptuncnv  22658  ptunhmeo  22659  filintn0  22712  trnei  22743  flimfil  22820  flimopn  22826  fbflim2  22828  cnpflf2  22851  flfcnp  22855  flfcnp2  22858  fclsopn  22865  fcfnei  22886  cnpfcf  22892  flfcntr  22894  alexsublem  22895  ptcmplem3  22905  ptcmplem4  22906  cnextfres1  22919  tmdcn2  22940  tmdgsum  22946  tmdgsum2  22947  efmndtmd  22952  symgtgp  22957  tgphaus  22968  tgpt1  22969  qustgplem  22972  prdstmdd  22975  prdstgpd  22976  haustsms  22987  tsmscls  22989  tsmsmhm  22997  tsmsadd  22998  tgptsmscls  23001  tsmssplit  23003  restutop  23089  utopreg  23104  ressusp  23116  ucncn  23136  xmetunirn  23189  ressprdsds  23223  xpsdsval  23233  xblss2ps  23253  blbas  23282  mopntopon  23291  isxms2  23300  imasf1oxms  23341  imasf1oms  23342  prdsxmslem2  23381  tmsxpsval  23390  tngngp2  23504  tngngp  23506  tgioo  23647  metdseq0  23705  cncfmpt2f  23766  cncfcnvcn  23776  cnmptre  23778  cnheibor  23806  nmhmcn  23971  cvsdiv  23983  cvsdivcl  23984  cphsubrglem  24028  cphreccllem  24029  iscmet3  24144  relcmpcmet  24169  bcthlem4  24178  rrxds  24244  rrxvsca  24245  rrxplusgvscavalb  24246  rrxbasefi  24261  rrxmetfi  24263  minveclem4  24283  ivthicc  24309  evthicc  24310  ovolicc2lem4  24371  ovolicc2lem5  24372  iunmbl2  24408  vitalilem3  24461  cncombf  24509  cnmbf  24510  dvres2lem  24761  cpncn  24787  cpnres  24788  dvaddbr  24789  dvmulbr  24790  dvcobr  24797  dvcjbr  24800  dvrec  24806  dvcnvlem  24827  dvlip2  24846  dvivth  24861  lhop2  24866  lhop  24867  dvcnvrelem1  24868  dvcnvrelem2  24869  dvcnvre  24870  ftc1lem6  24892  mdegvscale  24927  mdegvsca  24928  fta1blem  25020  plyaddlem1  25061  plymullem1  25062  coeeulem  25072  tayl0  25208  taylthlem1  25219  taylthlem2  25220  ulmdvlem3  25248  psercnlem2  25270  psercn  25272  efsubm  25394  cxpcn3  25588  loglesqrt  25598  efrlim  25806  ppinprm  25988  chtnprm  25990  dchrptlem1  26099  dchrptlem2  26100  tgbtwnouttr2  26540  tgldim0eq  26548  tgifscgr  26553  iscgrglt  26559  ercgrg  26562  tgcgrxfr  26563  motcgrg  26589  tglngne  26595  tgcolg  26599  tgbtwnconn1lem2  26618  tgbtwnconn1lem3  26619  legtri3  26635  legbtwn  26639  ncolne1  26670  tgisline  26672  tglinethru  26681  coltr3  26693  colline  26694  tglowdim2ln  26696  mirinv  26711  miriso  26715  mirauto  26729  miduniq  26730  krippenlem  26735  midexlem  26737  ragperp  26762  footexALT  26763  footexlem2  26765  perpdragALT  26772  perpdrag  26773  colperpexlem1  26775  colperpexlem3  26777  mideulem2  26779  midex  26782  opphllem1  26792  opphllem3  26794  opphllem4  26795  hlpasch  26801  trgcopy  26849  f1otrg  26916  axlowdimlem16  27002  elntg  27029  eengtrkg  27031  eengtrkge  27032  clwwlkccatlem  28026  grpoidinv2  28550  grpoinv  28560  ubthlem2  28906  shuni  29335  acunirnmpt  30670  acunirnmpt2  30671  acunirnmpt2f  30672  fpwrelmap  30742  fzm1ne1  30784  fzom1ne1  30796  ccatf1  30897  swrdf1  30902  gsummpt2d  30982  gsumhashmul  30989  odpmco  31028  pmtrcnel  31031  pmtrcnel2  31032  pmtrcnelor  31033  tocyc01  31058  trsp2cyc  31063  cycpmco2f1  31064  cycpmco2rn  31065  cycpmco2lem1  31066  cycpmco2lem2  31067  cycpmco2lem3  31068  cycpmco2lem4  31069  cycpmco2lem5  31070  cycpmco2lem6  31071  cycpmco2lem7  31072  cycpmco2  31073  cycpmconjv  31082  cycpmrn  31083  tocyccntz  31084  rngurd  31155  freshmansdream  31157  pidlnz  31239  nsgmgc  31265  elrspunidl  31274  qsidomlem1  31296  idlsrg0g  31319  ply1chr  31337  srasubrg  31342  drgextlsp  31349  matdim  31366  lbslsat  31367  lindsunlem  31373  lbsdiflsp0  31375  dimkerim  31376  fedgmullem1  31378  fedgmullem2  31379  fedgmul  31380  fldexttr  31401  extdgmul  31404  extdg1id  31406  rspectopn  31485  zarclsiin  31489  zarmxt1  31498  rspectps  31501  rhmpreimacn  31503  ordtrest2NEWlem  31540  ordtrest2NEW  31541  lmxrge0  31570  nmmulg  31584  rrhcn  31613  esumadd  31691  esumaddf  31695  esumcocn  31714  measiuns  31851  mbfmco2  31898  dya2iocnrect  31914  omscl  31928  omsf  31929  oms0  31930  sibf0  31967  sibfof  31973  sitgaddlemb  31981  fibp1  32034  ccatmulgnn0dir  32187  cxpcncf1  32241  ftc2re  32244  fsum2dsub  32253  reprf  32258  reprsum  32259  bnj1450  32697  bnj1501  32714  revpfxsfxrev  32744  indispconn  32863  connpconn  32864  pconnpi1  32866  sconnpi1  32868  cvmsss2  32903  cvmliftmolem1  32910  cvmliftlem8  32921  cvmliftlem10  32923  cvmliftlem11  32924  cvmlift2lem9  32940  cvmlift2lem12  32943  cvmlift3lem7  32954  mrsubcv  33139  mrsubff  33141  mrsubccat  33147  elmrsubrn  33149  mrsubco  33150  mrsubvrs  33151  nodenselem5  33577  oldlim  33755  cofcutr  33778  linethru  34141  ivthALT  34210  neibastop2  34236  filnetlem4  34256  matunitlindflem2  35460  poimirlem1  35464  poimirlem2  35465  poimirlem8  35471  poimirlem9  35472  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem22  35485  poimirlem23  35486  poimir  35496  broucube  35497  areacirclem4  35554  fdc  35589  isbnd3  35628  prdsbnd  35637  prdstotbnd  35638  prdsbnd2  35639  rrnequiv  35679  reheibor  35683  iscringd  35842  isfldidl  35912  eqvrelth  36410  eqlkr  36799  ldualvsubval  36857  dvalveclem  38725  dia2dimlem5  38768  dia2dimlem9  38772  tendoinvcl  38804  dvhgrp  38807  dvhlveclem  38808  dihpN  39036  dochsnkr2cl  39174  lcfl7lem  39199  lclkr  39233  lclkrs  39239  lcfrvalsnN  39241  lcfrlem4  39245  lcfrlem6  39247  lcfrlem16  39258  lcdvsubval  39318  lcdlkreqN  39322  mapdcl2  39356  mapdincl  39361  mapdlsmcl  39363  mapdpglem3  39375  hdmaprnlem9N  39557  hdmaplkr  39613  hdmapip0  39615  hdmapglem7a  39627  sticksstones11  39781  sticksstones12a  39782  evlsscaval  39924  mhphf  39936  prjspnvs  40108  prjspner1  40112  fltnltalem  40143  diophin  40238  acongeq  40449  isnumbasgrplem2  40573  proot1mul  40668  iunrelexpuztr  40945  ntrclsiex  41281  ntrneiiex  41304  ntrneinex  41305  elnelneqd  41432  grurankcld  41465  bccbc  41577  suctrALT  42060  restuni3  42281  disjf1o  42343  disjinfi  42345  choicefi  42354  fsneq  42360  fsneqrn  42365  unirnmapsn  42368  iunmapsn  42371  monoords  42450  elfzolem1  42474  uzfissfz  42479  monoord2xrv  42640  evthiccabs  42650  iooabslt  42653  tgqioo2  42701  islptre  42778  limciccioolb  42780  sumnnodd  42789  limcicciooub  42796  lptre2pt  42799  limcresiooub  42801  limcresioolb  42802  lptioo1cn  42805  reclimc  42812  liminfvalxr  42942  liminfvaluz  42951  limsupvaluz3  42957  fsumcncf  43037  ioccncflimc  43044  cncfuni  43045  icccncfext  43046  cncficcgt0  43047  icocncflimc  43048  cncfdmsn  43049  cncfiooicclem1  43052  cncfiooicc  43053  cncfioobd  43056  cxpcncf2  43058  fprodsub2cncf  43064  fprodadd2cncf  43065  fperdvper  43078  dvcosax  43085  dvnmul  43102  dvnprodlem1  43105  dvnprodlem2  43106  itgsubsticclem  43134  fvvolioof  43148  fvvolicof  43150  stoweidlem26  43185  stoweidlem27  43186  stoweidlem31  43190  stoweidlem34  43193  dirkercncflem2  43263  dirkercncflem3  43264  dirkercncflem4  43265  dirkercncf  43266  fourierdlem16  43282  fourierdlem20  43286  fourierdlem21  43287  fourierdlem22  43288  fourierdlem26  43292  fourierdlem32  43298  fourierdlem33  43299  fourierdlem38  43304  fourierdlem39  43305  fourierdlem46  43311  fourierdlem48  43313  fourierdlem49  43314  fourierdlem53  43318  fourierdlem60  43325  fourierdlem61  43326  fourierdlem69  43334  fourierdlem70  43335  fourierdlem71  43336  fourierdlem73  43338  fourierdlem74  43339  fourierdlem75  43340  fourierdlem76  43341  fourierdlem80  43345  fourierdlem81  43346  fourierdlem82  43347  fourierdlem83  43348  fourierdlem84  43349  fourierdlem85  43350  fourierdlem88  43353  fourierdlem89  43354  fourierdlem91  43356  fourierdlem92  43357  fourierdlem93  43358  fourierdlem100  43365  fourierdlem101  43366  fourierdlem103  43368  fourierdlem104  43369  fourierdlem107  43372  fourierdlem111  43376  fourierdlem112  43377  fourierdlem113  43378  fouriersw  43390  fouriercn  43391  etransclem24  43417  etransclem26  43419  etransclem28  43421  etransclem31  43424  etransclem32  43425  etransclem33  43426  etransclem34  43427  etransclem35  43428  etransclem38  43431  rrxtopnfi  43446  rrxtoponfi  43450  qndenserrnbl  43454  qndenserrnopnlem  43456  qndenserrn  43458  rrnprjdstle  43460  ioorrnopnlem  43463  prsal  43477  intsaluni  43486  salgencntex  43500  subsaliuncllem  43514  fge0iccico  43526  sge0sn  43535  sge0tsms  43536  sge0cl  43537  sge0f1o  43538  sge0pr  43550  sge0isum  43583  nnfoctbdjlem  43611  iundjiunlem  43615  iundjiun  43616  meadjiunlem  43621  psmeasure  43627  meaiininclem  43642  caragenelss  43657  omeunile  43661  carageniuncllem1  43677  carageniuncllem2  43678  0ome  43685  isomenndlem  43686  isomennd  43687  hoicvr  43704  ovnpnfelsup  43715  ovncvrrp  43720  ovnsubaddlem1  43726  hoidmv1le  43750  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  hoidmvle  43756  ovnhoilem1  43757  hoi2toco  43763  ovncvr2  43767  hspdifhsp  43772  voncmpl  43777  hoiqssbl  43781  hspmbllem2  43783  hspmbl  43785  hoimbllem  43786  opnvonmbllem2  43789  mblvon  43795  ovolval3  43803  ovolval4lem1  43805  ovnovollem1  43812  ovnovollem2  43813  vonsn  43847  issmflem  43878  sssmf  43889  issmflelem  43895  issmfgtlem  43906  issmfgt  43907  smfaddlem1  43913  issmfgelem  43919  smflimlem3  43923  smfmullem2  43941  smfmullem4  43943  smfsuplem1  43959  smfsupmpt  43963  smfinfmpt  43967  smflimsuplem2  43969  smflimsuplem4  43971  smflimsupmpt  43977  smfliminfmpt  43980  fzoopth  44435  issubmgm2  44960  zlmodzxzel  45307  ply1mulgsum  45347  catprs  45908  thincmod  45928  mndtcob  45983  mndtccatid  45988  mndtcid  45990  grptcmon  45991  grptcepi  45992