Theorem eleqtrrdi 2842

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
eleqtrrdi.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrrdi.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleqtrrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrdi

Step	Hyp	Ref	Expression
1		eleqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2740	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2841	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  3eltr4g  2848  brelrng  5880  elabrex  7176  elabrexg  7177  fliftel1  7244  ovidig  7488  unielxp  7959  tfrlem11  8307  rdglim  8345  seqomlem4  8372  2oconcl  8418  ecopqsi  8695  erov  8738  eroprf  8739  sbthlem2  9001  dffi3  9315  ixpiunwdom  9476  cantnfcl  9557  r1lim  9665  rankwflemb  9686  pwwf  9700  unwf  9703  rankwflem  9708  uniwf  9712  rankpwi  9716  rankr1g  9725  r1pw  9738  r1rankid  9752  rankuni  9756  djulcl  9803  djurcl  9804  inlresf  9807  inrresf  9809  djuun  9819  cardlim  9865  infxpenlem  9904  alephfp  9999  cfsmolem  10161  alephsing  10167  hsmexlem4  10320  axdc3lem2  10342  numth3  10361  iunfo  10430  konigthlem  10459  iunctb  10465  canthwelem  10541  canthwe  10542  r1limwun  10627  inar1  10666  inatsk  10669  gruina  10709  grur1  10711  tskmval  10730  tskmcl  10732  pinq  10818  dmrecnq  10859  addclsr  10974  mulclsr  10975  axaddf  11036  axmulf  11037  peano2nn  12137  uztrn2  12751  eluz2nn  12786  peano2uzs  12800  uzsupss  12838  uzsup  13767  uzrdgfni  13865  uzrdgsuci  13867  fsuppmapnn0fiub  13898  seqf  13930  ser0  13961  bcm1k  14222  bcp1nk  14224  bcpasc  14228  hashprdifel  14305  fz1isolem  14368  pr2pwpr  14386  tpf  14406  ccats1val2  14535  rexuzre  15260  limsupgre  15388  climconst  15450  rlimclim1  15452  climrlim2  15454  clim2ser  15562  clim2ser2  15563  iserex  15564  isermulc2  15565  iserle  15567  isercolllem3  15574  isercoll2  15576  climsup  15577  iseraltlem2  15590  iseraltlem3  15591  zsum  15625  isumclim3  15666  isumadd  15674  fsump1i  15676  iserabs  15722  cvgcmp  15723  cvgcmpub  15724  cvgcmpce  15725  abscvgcvg  15726  isumshft  15746  isumsplit  15747  isum1p  15748  isumrpcl  15750  isumsup2  15753  climcndslem1  15756  cvgrat  15790  clim2prod  15795  clim2div  15796  prodf1  15798  ntrivcvgn0  15805  ntrivcvgtail  15807  fprodntriv  15849  fprodabs  15881  fprodeq0  15882  iprodclim3  15907  iprodmul  15910  ef0lem  15985  fprodefsum  16002  rpnnen2lem3  16125  dvdsflip  16228  fzo0dvdseq  16234  bitsinv1  16353  smupval  16399  smueqlem  16401  seq1st  16482  algr0  16483  prmind2  16596  crth  16689  eulerthlem2  16693  prmdiv  16696  pockthlem  16817  pockthg  16818  unbenlem  16820  prmunb  16826  prmgaplem7  16969  strfv2d  17112  imasvscaval  17442  oppccatid  17625  oppccatf  17634  epii  17650  fthepi  17837  funcestrcsetclem3  18048  funcsetcestrclem3  18062  yon12  18171  yon2  18172  yonedalem4c  18183  yonedalem22  18184  yonedalem3b  18185  yonedainv  18187  acsmapd  18460  chnub  18528  chnccats1  18531  chnccat  18532  mgm2nsgrplem1  18826  mgm2nsgrplem2  18827  mgm2nsgrplem3  18828  sgrp2nmndlem1  18831  sgrp2rid2  18834  ghmqusker  19199  cntrsubgnsg  19255  symgpssefmnd  19308  pmtrrn  19369  gexcl3  19499  efgi  19631  efgi2  19637  efgs1b  19648  efgredlemg  19654  efgredlemd  19656  frgpnabllem1  19785  cycsubgcyg  19813  gsumzaddlem  19833  dprdwd  19925  dprd2da  19956  rhmopp  20424  lsppratlem3  21086  lsppratlem4  21087  lbsextlem2  21096  lidl0ALT  21165  lidl1ALT  21168  2idl0  21197  2idl1  21198  domnchr  21469  znf1o  21488  mplsubrglem  21941  mpfconst  22036  mpfproj  22037  mpfind  22042  mhpmulcl  22064  pf1const  22261  pf1id  22262  mpfpf1  22266  pf1mpf  22267  madetsumid  22376  slesolex  22597  pmatcoe1fsupp  22616  mat2pmatbas0  22642  pmatcollpw  22696  pm2mpf1  22714  isclo  23002  indiscld  23006  restntr  23097  ordtbaslem  23103  ordtbas2  23106  lmconst  23176  lmss  23213  conncompid  23346  2ndcomap  23373  locfincmp  23441  comppfsc  23447  xkouni  23514  txcls  23519  ptclsg  23530  uptx  23540  txindis  23549  tx1stc  23565  cnmpt1res  23591  tgqtop  23627  uffix  23836  cnpflf2  23915  ptcmplem2  23968  ptcmplem4  23970  tgpconncomp  24028  tsmsfbas  24043  fmucnd  24206  prdsxmetlem  24283  imasdsf1olem  24288  prdsbl  24406  blcvx  24713  xrsmopn  24728  xrge0tsms  24750  metdcn2  24755  expcncf  24847  cnmpopc  24849  icchmeo  24865  icchmeoOLD  24866  iccpnfhmeo  24870  cnheibor  24881  evth  24885  evth2  24886  lebnumlem2  24888  lebnumii  24892  reparphti  24923  reparphtiOLD  24924  cfilfcls  25201  minveclem2  25353  minveclem3  25356  minveclem4  25359  ovoliunlem1  25430  ovolicc1  25444  iundisj  25476  volsup  25484  uniioombllem3  25513  vitalilem2  25537  vitalilem3  25538  mbfsup  25592  mbfinf  25593  mbflimsup  25594  itg2monolem1  25678  limcflflem  25808  limccnp  25819  limccnp2  25820  dvidlem  25843  dvn2bss  25859  cpnres  25866  dvcobr  25876  dvcobrOLD  25877  dvrec  25886  c1liplem1  25928  dvcnvrelem2  25950  dvfsumrlimf  25958  dvfsumlem1  25959  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem3  25962  dvfsumlem4  25963  dvfsumrlim  25965  dvfsum2  25968  coeeulem  26156  coeid3  26172  plycn  26193  plycnOLD  26194  dvntaylp  26306  taylthlem1  26308  taylthlem2  26309  taylthlem2OLD  26310  ulm2  26321  ulmshftlem  26325  ulmshft  26326  ulm0  26327  ulmcn  26335  ulmdvlem3  26338  ulmdv  26339  mtest  26340  mtestbdd  26341  dvradcnv  26357  psercn2  26359  psercn2OLD  26360  psercn  26363  pserdv  26366  abelth  26378  efif1olem2  26479  efif1olem4  26481  efifo  26483  eff1olem  26484  logcn  26583  dvloglem  26584  cxpcn3  26685  resqrtcn  26686  sqrtcn  26687  logbleb  26720  logblt  26721  asinneg  26823  atanlogsub  26853  atanbnd  26863  ressatans  26871  leibpilem2  26878  xrlimcnp  26905  efrlim  26906  efrlimOLD  26907  scvxcvx  26923  ppiub  27142  chtub  27150  logexprlim  27163  lgseisenlem1  27313  rplogsumlem1  27422  rplogsumlem2  27423  dchrisumlem2  27428  dchrisum0flb  27448  logdivbnd  27494  pntlem3  27547  dfnns2  28297  tgcgr4  28509  ltgov  28575  f1otrg  28849  eengtrkg  28964  iedgedg  29028  ushgredgedgloop  29209  subgruhgredgd  29262  uvtxupgrres  29386  umgr2v2evd2  29506  edginwlk  29613  wlk1walk  29617  crctcshwlkn0lem6  29793  wlkiswwlks1  29845  minvecolem1  30854  minvecolem2  30855  minvecolem4  30860  htthlem  30897  5oalem2  31635  3oalem2  31643  iundisjf  32569  fmptco1f1o  32615  xppreima  32627  xppreima2  32633  dfcnv2  32658  ccatws1f1o  32932  gsumhashmul  33041  xrge0tsmsd  33042  gsumwrd2dccatlem  33046  odpmco  33055  pmtrcnelor  33060  fzo0pmtrlast  33061  wrdpmtrlast  33062  pmtrto1cl  33068  psgnfzto1stlem  33069  fzto1stfv1  33070  fzto1st  33072  fzto1stinvn  33073  psgnfzto1st  33074  tocycf  33086  cycpmco2lem7  33101  cycpmco2  33102  cycpmrn  33112  cyc3evpm  33119  cyc3genpmlem  33120  cycpmgcl  33122  cyc3conja  33126  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnlem4  33212  elrgspnsubrunlem1  33214  nsgmgc  33377  nsgqusf1olem1  33378  nsgqusf1olem2  33379  rhmpreimaprmidl  33416  ssdifidllem  33421  ssdifidl  33422  ssmxidllem  33438  drngmxidlr  33443  opprqus1r  33457  qsdrngilem  33459  qsdrngi  33460  rsprprmprmidlb  33488  rprmirredb  33497  1arithufdlem1  33509  1arithufdlem2  33510  1arithufdlem3  33511  1arithufdlem4  33512  fply1  33521  ply1degltel  33555  ply1degleel  33556  ply1degltlss  33557  esplylem  33587  esplyfv1  33590  esplysply  33592  ply1degltdimlem  33635  ply1degltdim  33636  algextdeglem4  33733  algextdeglem6  33735  algextdeglem7  33736  algextdeglem8  33737  nn0constr  33774  smatlem  33810  smatcl  33815  zartopn  33888  zarmxt1  33893  tpr2rico  33925  xrmulc1cn  33943  xrge0mulc1cn  33954  esumpfinvallem  34087  ldgenpisyslem1  34176  dynkin  34180  brfae  34261  sxbrsigalem3  34285  dya2icoseg2  34291  omsmeas  34336  sibfof  34353  sseqmw  34404  sseqf  34405  sseqp1  34408  fiblem  34411  fibp1  34414  probfinmeasbALTV  34442  repr0  34624  reprpmtf1o  34639  hgt750lemg  34667  bnj1379  34842  srcmpltd  35092  fineqvnttrclselem3  35143  subfacp1lem5  35228  subfacp1lem6  35229  cvxpconn  35286  cvxsconn  35287  cvmliftlem6  35334  cvmliftlem8  35336  cvmliftlem10  35338  cvmlift2lem6  35352  cvmlift2lem11  35357  cvmlift2lem12  35358  2goelgoanfmla1  35468  prv1n  35475  msubff  35574  msubco  35575  elmsta  35592  msubff1  35600  mvhf  35602  msubvrs  35604  iprodefisumlem  35784  filnetlem3  36424  knoppcnlem10  36546  knoppcnlem11  36547  icoreunrn  37403  icoreelrn  37405  ralssiun  37451  poimirlem3  37673  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem30  37700  dvasin  37754  cover2  37765  upixp  37779  sdclem1  37793  fdc  37795  caushft  37811  ismtyres  37858  rrncmslem  37882  isfld2  38055  presuc  38520  osumcllem10N  40074  pexmidlem7N  40085  dihglblem2N  41403  lcfrvalsnN  41650  lcfrlem5  41655  lcfrlem6  41656  lcfrlem27  41678  lcfrlem37  41688  aks6d1c1p4  42214  aks6d1c1p7  42216  aks6d1c1p8  42218  evl1gprodd  42220  aks6d1c2lem4  42230  aks6d1c5lem3  42240  aks6d1c6lem2  42274  prjspvs  42713  0prjspnrel  42730  monotuz  43044  expdiophlem1  43124  kelac2  43168  naddwordnexlem4  43504  grurankcld  44336  dvgrat  44415  nzss  44420  uzmptshftfval  44449  binomcxplemnotnn0  44459  orbitinit  45059  orbitcl  45060  permaxinf2lem  45115  refsumcn  45137  rfcnpre2  45138  rfcnpre3  45140  rfcnpre4  45141  disjf1o  45298  unirnmap  45315  unirnmapsn  45321  ssmapsn  45323  mptssid  45348  allbutfi  45501  eluzd  45517  uzidd2  45524  ressiocsup  45664  ressioosup  45665  ressiooinf  45667  fsumsermpt  45689  climexp  45715  climinf  45716  climsuse  45718  sumnnodd  45740  limsupresico  45808  limsupubuzlem  45820  limsupresxr  45874  liminfresxr  45875  liminfresico  45879  limsup10exlem  45880  cnrefiisplem  45937  cncfiooicclem1  46001  dvsinax  46021  itgsinexplem1  46062  fvvolioof  46097  fvvolicof  46099  stoweidlem14  46122  stoweidlem16  46124  stoweidlem31  46139  stoweidlem34  46142  stoweidlem36  46144  stoweidlem43  46151  stoweidlem46  46154  stoweidlem47  46155  stoweidlem52  46160  stoweidlem55  46163  stoweidlem57  46165  dirkercncf  46215  fourierdlem20  46235  fourierdlem42  46257  fourierdlem48  46262  fourierdlem49  46263  fourierdlem51  46265  fourierdlem54  46268  fourierdlem62  46276  fourierdlem71  46285  fourierdlem80  46294  fourierdlem114  46328  fouriersw  46339  ioorrnopnlem  46412  ioorrnopnxrlem  46414  salexct3  46450  salgencntex  46451  salgensscntex  46452  subsalsal  46467  sge0fodjrnlem  46524  sge0isum  46535  sge0seq  46554  sge0reuz  46555  sge0reuzb  46556  meadjiunlem  46573  meaiininclem  46594  carageniuncllem1  46629  caratheodorylem1  46634  hoiprodp1  46696  hoidmv1lelem1  46699  hoidmv1lelem2  46700  hoidmv1le  46702  hoidmvlelem1  46703  hoidmvlelem2  46704  hoidmvlelem3  46705  voncmpl  46729  hoiqssbl  46733  smflimlem2  46880  smfsuplem1  46919  smfsuplem3  46921  fsupdm  46950  finfdm  46954  cfsetsnfsetf  47168  fcores  47177  afvres  47282  afv2res  47349  fundcmpsurinjimaid  47521  iccpartigtl  47533  sprsymrelf  47605  prproropf1olem2  47614  uhgrimedgi  48000  isuspgrim0lem  48003  isuspgrimlem  48005  ushggricedg  48037  grimedg  48045  usgrgrtrirex  48060  isubgr3stgrlem7  48082  uspgrlimlem4  48101  grlimprclnbgr  48106  gpgiedgdmellem  48156  gpg3kgrtriex  48199  funcringcsetcALTV2lem3  48402  funcringcsetclem3ALTV  48425  lindslinindsimp2lem5  48573  rrxsphere  48859  line2  48863  iooii  49028  icccldii  49029  iscnrm3rlem3  49052  eloppf2  49245  oppcup  49318  natoppf  49340  zeroo2  49345  oppfdiag1  49525  oppfdiag  49527  2arwcat  49711  incat  49712  lmddu  49778  onsetreclem3  49818  amgmwlem  49913