Theorem eleqtrd 2846

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eleqtrrd  2847  eleqtrid  2850  eleqtrdi  2854  3eltr3d  2858  prel12g  4888  opth1  5495  0nelop  5515  fvelimad  6989  fviss  6999  feldmfvelcdm  7120  tfisi  7896  fnwelem  8172  frrlem8  8334  frrlem10  8336  fprresex  8351  wfrlem17OLD  8381  omeulem1  8638  oeeulem  8657  oeeui  8658  oaabs2  8705  omabs  8707  ercl  8774  erth  8814  ecelqsdm  8845  ordtypelem6  9592  ordtypelem7  9593  cantnfval  9737  cantnfp1lem3  9749  cantnflem4  9761  r1pwss  9853  rankonidlem  9897  rankxplim3  9950  fseqenlem2  10094  iunfictbso  10183  dfac12lem1  10213  dfac12lem2  10214  fin23lem30  10411  iundom2g  10609  fpwwe2lem5  10704  fpwwe2lem8  10707  lincmb01cmp  13555  fzopth  13621  fzoaddel2  13772  fzosubel2  13776  fzocatel  13780  zpnn0elfzo1  13790  fzoend  13807  fzoopth  13812  peano2fzor  13824  monoord2  14084  sermono  14085  expmulnbnd  14284  bcpasc  14370  hash1elsn  14420  swrdcl  14693  revcl  14809  revlen  14810  fsum0diag2  15831  isumsplit  15888  fprodser  15997  sadadd  16513  sadass  16517  smuval2  16528  smumul  16539  vdwapun  17021  vdwlem9  17036  ramub1lem1  17073  prdsbasfn  17531  prdsbasprj  17532  pwsplusgval  17550  pwsmulrval  17551  pwsvscafval  17554  xpsaddlem  17633  xpsvsca  17637  xpsle  17639  mreexmrid  17701  homfeqval  17755  comfval2  17761  comfeq  17764  comfeqval  17766  oppccomfpropd  17787  invco  17832  sectepi  17845  issubc3  17913  funcf2  17932  fthepi  17995  nat1st2nd  18019  homarcl2  18102  coapm  18138  setcmon  18154  setcepi  18155  setcsect  18156  setcinv  18157  setciso  18158  cat1lem  18163  catccatid  18173  resscatc  18176  catciso  18178  catcbascl  18179  catcoppccl  18184  catcoppcclOLD  18185  catcfuccl  18186  catcfucclOLD  18187  xpccatid  18257  catcxpccl  18276  catcxpcclOLD  18277  xpcpropd  18278  evlfcl  18292  curfpropd  18303  hofcl  18329  yonedalem3  18350  yonffthlem  18352  poslubdg  18484  grpidd  18709  gsumress  18720  issubmgm2  18741  sgrppropd  18769  ismndd  18794  mndpropd  18797  issubmnd  18799  submnd0  18801  imasmnd  18810  xpsmnd0  18813  frmdelbas  18888  grpidd2  19017  pwsinvg  19093  imasgrp  19096  xpsinv  19100  xpsgrpsub  19101  ressmulgnnd  19118  submmulg  19158  subginvcl  19175  subgcl  19176  subgsub  19178  subgmulg  19180  1nsgtrivd  19214  quseccl0  19225  kerf1ghm  19287  ghmqusnsglem1  19320  ghmquskerlem1  19323  ghmquskerco  19324  ghmqusker  19327  gaid2  19343  finodsubmsubg  19609  submod  19611  odsubdvds  19613  sylow1lem4  19643  sylow2alem2  19660  lsmdisj2  19724  subgdisj1  19733  pj1id  19741  efgsrel  19776  efgrelexlemb  19792  efgcpbl2  19799  frgpcpbl  19801  frgp0  19802  frgpeccl  19803  frgpadd  19805  frgpup3lem  19819  frgpnabllem1  19915  cycsubgcyg  19943  prdsgsum  20023  dprdfeq0  20066  dmdprdsplitlem  20081  dpjidcl  20102  pgpfac1lem3a  20120  pgpfac1lem4  20122  pgpfaclem1  20125  pgpfaclem2  20126  ablfaclem2  20130  simpgnsgeqd  20145  simpgnsgbid  20147  ablsimpnosubgd  20148  rngpropd  20201  imasrng  20204  ringurd  20212  ringidss  20300  ringpropd  20311  imasring  20353  xpsring1d  20356  qusring2  20357  lringuplu  20570  subrngmcl  20583  subrg1  20610  subrgdv  20617  subrgunit  20618  resrhm  20629  issubdrg  20803  lmodprop2d  20944  0lmhm  21062  lmhmpropd  21095  lspfixed  21153  lssacsex  21169  lbsextlem4  21186  quscrng  21316  qusmulcrng  21317  rhmqusnsg  21318  rngqiprngimf  21330  rngqiprngimfo  21334  rngqiprngfulem4  21347  znf1o  21593  freshmansdream  21616  psgnghm2  21622  elocv  21709  pjff  21755  frlmlss  21794  frlmsubgval  21808  frlmvscafval  21809  frlmvscavalb  21813  frlmvplusgscavalb  21814  frlmphl  21824  uvcresum  21836  frlmssuvc1  21837  frlmssuvc2  21838  frlmsslsp  21839  frlmup1  21841  sraassab  21911  assapropd  21915  psrelbas  21977  resspsrvsca  22020  subrgpsr  22021  psrascl  22022  mplcoe1  22078  mplbas2  22083  mplascl  22111  mplmon2cl  22115  mplmon2mul  22116  evlrhm  22143  mpfconst  22148  mhprcl  22170  mhpvscacl  22181  psdascl  22195  vr1cl2  22215  ply1lss  22219  ply1subrg  22220  psropprmul  22260  ply1chr  22331  evl1vsd  22369  evl1expd  22370  evl1gsumadd  22383  evl1gsummon  22390  evls1fpws  22394  evls1vsca  22398  asclply1subcl  22399  evls1maplmhm  22402  evl1maprhm  22404  ply1vscl  22409  matring  22470  matassa  22471  mat1  22474  mattposcl  22480  mavmulass  22576  mdetunilem9  22647  matinv  22704  cpmadugsumlemF  22903  cpmadugsumfi  22904  cpmidgsum2  22906  elcls3  23112  mreclatdemoBAD  23125  neiptopnei  23161  resstps  23216  ordtrest2lem  23232  ordtrest2  23233  pnfnei  23249  mnfnei  23250  iscnp2  23268  iscnp4  23292  cnrest2r  23316  lmcls  23331  lmcld  23332  cnt0  23375  cnhaus  23383  isreg2  23406  connclo  23444  1stccnp  23491  loclly  23516  lly1stc  23525  locfincmp  23555  unisngl  23556  comppfsc  23561  kgencmp2  23575  llycmpkgen2  23579  kgen2ss  23584  kgencn3  23587  pttoponconst  23626  txcls  23633  txbasval  23635  dfac14lem  23646  ptcn  23656  ptrescn  23668  txtube  23669  txcmplem1  23670  txlm  23677  txkgen  23681  xkopjcn  23685  cnmptkp  23709  xkoinjcn  23716  qtopkgen  23739  imastps  23750  isr0  23766  r0cld  23767  pt1hmeo  23835  ptuncnv  23836  ptunhmeo  23837  filintn0  23890  trnei  23921  flimfil  23998  flimopn  24004  fbflim2  24006  cnpflf2  24029  flfcnp  24033  flfcnp2  24036  fclsopn  24043  fcfnei  24064  cnpfcf  24070  flfcntr  24072  alexsublem  24073  ptcmplem3  24083  ptcmplem4  24084  cnextfres1  24097  tmdcn2  24118  tmdgsum  24124  tmdgsum2  24125  efmndtmd  24130  symgtgp  24135  tgphaus  24146  tgpt1  24147  qustgplem  24150  prdstmdd  24153  prdstgpd  24154  haustsms  24165  tsmscls  24167  tsmsmhm  24175  tsmsadd  24176  tgptsmscls  24179  tsmssplit  24181  restutop  24267  utopreg  24282  ressusp  24294  ucncn  24315  xmetunirn  24368  ressprdsds  24402  xpsdsval  24412  xblss2ps  24432  blbas  24461  mopntopon  24470  isxms2  24479  imasf1oxms  24523  imasf1oms  24524  prdsxmslem2  24563  tmsxpsval  24572  tngngp2  24694  tngngp  24696  tgioo  24837  metdseq0  24895  cncfmpt2f  24960  cncfcnvcn  24971  cnmptre  24973  cnheibor  25006  nmhmcn  25172  cvsdiv  25184  cvsdivcl  25185  cphsubrglem  25230  cphreccllem  25231  iscmet3  25346  relcmpcmet  25371  bcthlem4  25380  rrxds  25446  rrxvsca  25447  rrxplusgvscavalb  25448  rrxbasefi  25463  rrxmetfi  25465  minveclem4  25485  mulcncf  25499  ivthicc  25512  evthicc  25513  ovolicc2lem4  25574  ovolicc2lem5  25575  iunmbl2  25611  vitalilem3  25664  cncombf  25712  cnmbf  25713  dvres2lem  25965  cpncn  25992  cpnres  25993  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvcjbr  26007  dvrec  26013  dvcnvlem  26034  dvlip2  26054  dvivth  26069  lhop2  26074  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  ftc1lem6  26102  mdegvscale  26134  mdegvsca  26135  fta1blem  26230  plyaddlem1  26272  plymullem1  26273  coeeulem  26283  tayl0  26421  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmdvlem3  26463  psercnlem2  26486  psercn  26488  efsubm  26611  cxpcn3  26809  loglesqrt  26822  efrlim  27030  efrlimOLD  27031  ppinprm  27213  chtnprm  27215  dchrptlem1  27326  dchrptlem2  27327  nodenselem5  27751  oldlim  27943  cofcutr  27976  addsproplem6  28025  negsproplem6  28083  mulsproplem13  28172  mulsproplem14  28173  noseqp1  28315  tgbtwnouttr2  28521  tgldim0eq  28529  tgifscgr  28534  iscgrglt  28540  ercgrg  28543  tgcgrxfr  28544  motcgrg  28570  tglngne  28576  tgcolg  28580  tgbtwnconn1lem2  28599  tgbtwnconn1lem3  28600  legtri3  28616  legbtwn  28620  ncolne1  28651  tgisline  28653  tglinethru  28662  coltr3  28674  colline  28675  tglowdim2ln  28677  mirinv  28692  miriso  28696  mirauto  28710  miduniq  28711  krippenlem  28716  midexlem  28718  ragperp  28743  footexALT  28744  footexlem2  28746  perpdragALT  28753  perpdrag  28754  colperpexlem1  28756  colperpexlem3  28758  mideulem2  28760  midex  28763  opphllem1  28773  opphllem3  28775  opphllem4  28776  hlpasch  28782  trgcopy  28830  f1otrg  28897  axlowdimlem16  28990  elntg  29017  eengtrkg  29019  eengtrkge  29020  clwwlkccatlem  30021  grpoidinv2  30547  grpoinv  30557  ubthlem2  30903  shuni  31332  acunirnmpt  32677  acunirnmpt2  32678  acunirnmpt2f  32679  fpwrelmap  32747  fzm1ne1  32794  fzom1ne1  32806  ccatf1  32915  swrdf1  32923  pfxchn  32982  chnind  32983  chnub  32984  gsummpt2d  33032  gsumhashmul  33040  odpmco  33079  pmtrcnel  33082  pmtrcnel2  33083  pmtrcnelor  33084  tocyc01  33111  trsp2cyc  33116  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem1  33119  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  cycpmconjv  33135  cycpmrn  33136  tocyccntz  33137  0ringcring  33224  rloccring  33242  rloc0g  33243  rloc1r  33244  isdrng4  33264  sdrgdvcl  33266  sdrginvcl  33267  fracfld  33275  lpirlidllpi  33367  pidlnz  33369  nsgmgc  33405  rhmquskerlem  33418  elrspunidl  33421  elrspunsn  33422  drngidl  33426  qsidomlem1  33445  mxidlirred  33465  drngmxidlr  33471  opprmxidlabs  33480  opprqusplusg  33482  opprqusmulr  33484  opprqusdrng  33486  qsdrngilem  33487  qsdrngi  33488  qsdrnglem2  33489  qsdrng  33490  qsfld  33491  idlsrg0g  33499  1arithidomlem2  33529  ressdeg1  33556  ressply1invg  33559  ressply1sub  33560  ressasclcl  33561  ply1degltlss  33582  gsummoncoe1fzo  33583  ig1pmindeg  33587  q1pvsca  33589  r1pvsca  33590  srasubrg  33599  drgextlsp  33608  matdim  33628  lbslsat  33629  ply1degltdimlem  33635  ply1degltdim  33636  lindsunlem  33637  lbsdiflsp0  33639  dimkerim  33640  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  fldexttr  33671  extdgmul  33674  extdg1id  33676  irngss  33687  irngnzply1lem  33690  irngnzply1  33691  irngnminplynz  33705  algextdeglem4  33711  algextdeglem8  33715  rtelextdg2lem  33717  rtelextdg2  33718  constrconj  33735  rspectopn  33813  zarclsiin  33817  zarmxt1  33826  rspectps  33829  rhmpreimacn  33831  ordtrest2NEWlem  33868  ordtrest2NEW  33869  lmxrge0  33898  nmmulg  33914  rrhcn  33943  esumadd  34021  esumaddf  34025  esumcocn  34044  measiuns  34181  mbfmco2  34230  dya2iocnrect  34246  omscl  34260  omsf  34261  oms0  34262  sibf0  34299  sibfof  34305  sitgaddlemb  34313  fibp1  34366  ccatmulgnn0dir  34519  cxpcncf1  34572  ftc2re  34575  fsum2dsub  34584  reprf  34589  reprsum  34590  bnj1450  35026  bnj1501  35043  revpfxsfxrev  35083  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  36301  neibastop2  36327  filnetlem4  36347  weiunfr  36433  matunitlindflem2  37577  poimirlem1  37581  poimirlem2  37582  poimirlem8  37588  poimirlem9  37589  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimir  37613  broucube  37614  areacirclem4  37671  fdc  37705  isbnd3  37744  prdsbnd  37753  prdstotbnd  37754  prdsbnd2  37755  rrnequiv  37795  reheibor  37799  iscringd  37958  isfldidl  38028  eqvrelth  38567  eqlkr  39055  ldualvsubval  39113  dvalveclem  40982  dia2dimlem5  41025  dia2dimlem9  41029  tendoinvcl  41061  dvhgrp  41064  dvhlveclem  41065  dihpN  41293  dochsnkr2cl  41431  lcfl7lem  41456  lclkr  41490  lclkrs  41496  lcfrvalsnN  41498  lcfrlem4  41502  lcfrlem6  41504  lcfrlem16  41515  lcdvsubval  41575  lcdlkreqN  41579  mapdcl2  41613  mapdincl  41618  mapdlsmcl  41620  mapdpglem3  41632  hdmaprnlem9N  41814  hdmaplkr  41870  hdmapip0  41872  hdmapglem7a  41884  zndvdchrrhm  41927  remexz  42061  primrootspoweq0  42063  aks6d1c1p3  42067  aks6d1c1p5  42069  aks6d1c2lem4  42084  idomnnzpownz  42089  idomnnzgmulnz  42090  ringexp0nn  42091  aks6d1c5lem0  42092  aks6d1c5lem3  42094  aks6d1c5lem2  42095  aks6d1c5  42096  sticksstones11  42113  sticksstones12a  42114  sticksstones19  42122  aks6d1c6lem2  42128  aks6d1c6lem4  42130  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  aks6d1c6lem5  42134  aks5lem2  42144  ply1asclzrhval  42145  rhmpsr1  42508  evlsscaval  42519  selvvvval  42540  evlselv  42542  mhphf2  42553  mhphf4  42555  prjspnvs  42575  prjspnn0  42577  prjspner1  42581  fltnltalem  42617  diophin  42728  acongeq  42940  isnumbasgrplem2  43061  proot1mul  43155  oacl2g  43292  omabs2  43294  omcl2  43295  iunrelexpuztr  43681  ntrclsiex  44015  ntrneiiex  44038  ntrneinex  44039  elnelneqd  44164  grurankcld  44202  bccbc  44314  suctrALT  44797  restuni3  45020  disjf1o  45098  disjinfi  45099  choicefi  45107  fsneq  45113  fsneqrn  45118  unirnmapsn  45121  iunmapsn  45124  monoords  45212  elfzolem1  45236  uzfissfz  45241  monoord2xrv  45399  evthiccabs  45414  iooabslt  45417  tgqioo2  45465  islptre  45540  limciccioolb  45542  sumnnodd  45551  limcicciooub  45558  lptre2pt  45561  limcresiooub  45563  limcresioolb  45564  lptioo1cn  45567  reclimc  45574  liminfvalxr  45704  liminfvaluz  45713  limsupvaluz3  45719  fsumcncf  45799  ioccncflimc  45806  cncfuni  45807  icccncfext  45808  cncficcgt0  45809  icocncflimc  45810  cncfdmsn  45811  cncfiooicclem1  45814  cncfiooicc  45815  cncfioobd  45818  cxpcncf2  45820  fprodsub2cncf  45826  fprodadd2cncf  45827  fperdvper  45840  dvcosax  45847  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  itgsubsticclem  45896  fvvolioof  45910  fvvolicof  45912  stoweidlem26  45947  stoweidlem27  45948  stoweidlem31  45952  stoweidlem34  45955  dirkercncflem2  46025  dirkercncflem3  46026  dirkercncflem4  46027  dirkercncf  46028  fourierdlem16  46044  fourierdlem20  46048  fourierdlem21  46049  fourierdlem22  46050  fourierdlem26  46054  fourierdlem32  46060  fourierdlem33  46061  fourierdlem38  46066  fourierdlem39  46067  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem53  46080  fourierdlem60  46087  fourierdlem61  46088  fourierdlem69  46096  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem80  46107  fourierdlem81  46108  fourierdlem82  46109  fourierdlem83  46110  fourierdlem84  46111  fourierdlem85  46112  fourierdlem88  46115  fourierdlem89  46116  fourierdlem91  46118  fourierdlem92  46119  fourierdlem93  46120  fourierdlem100  46127  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fouriersw  46152  fouriercn  46153  etransclem24  46179  etransclem26  46181  etransclem28  46183  etransclem31  46186  etransclem32  46187  etransclem33  46188  etransclem34  46189  etransclem35  46190  etransclem38  46193  rrxtopnfi  46208  rrxtoponfi  46212  qndenserrnbl  46216  qndenserrnopnlem  46218  qndenserrn  46220  rrnprjdstle  46222  ioorrnopnlem  46225  prsal  46239  intsaluni  46250  salgencntex  46264  subsaliuncllem  46278  fge0iccico  46291  sge0sn  46300  sge0tsms  46301  sge0cl  46302  sge0f1o  46303  sge0pr  46315  sge0isum  46348  nnfoctbdjlem  46376  iundjiunlem  46380  iundjiun  46381  meadjiunlem  46386  psmeasure  46392  meaiininclem  46407  caragenelss  46422  omeunile  46426  carageniuncllem1  46442  carageniuncllem2  46443  0ome  46450  isomenndlem  46451  isomennd  46452  hoicvr  46469  ovnpnfelsup  46480  ovncvrrp  46485  ovnsubaddlem1  46491  hoidmv1le  46515  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvle  46521  ovnhoilem1  46522  hoi2toco  46528  ovncvr2  46532  hspdifhsp  46537  voncmpl  46542  hoiqssbl  46546  hspmbllem2  46548  hspmbl  46550  hoimbllem  46551  opnvonmbllem2  46554  mblvon  46560  ovolval3  46568  ovolval4lem1  46570  ovnovollem1  46577  ovnovollem2  46578  vonsn  46612  issmflem  46648  sssmf  46659  issmflelem  46665  issmfgtlem  46676  issmfgt  46677  smfaddlem1  46684  issmfgelem  46690  smflimlem3  46694  smfmullem2  46713  smfmullem4  46715  smfsuplem1  46732  smfsupmpt  46736  smfinfmpt  46740  smflimsuplem2  46742  smflimsuplem4  46744  smflimsupmpt  46750  smfliminfmpt  46753  fsupdm  46763  finfdm  46767  zlmodzxzel  48080  ply1mulgsum  48119  catprs  48678  thincmod  48698  mndtcob  48755  mndtccatid  48760  mndtcid  48762  grptcmon  48763  grptcepi  48764