Theorem eleqtrrdi 2849

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 2743	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2848	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  3eltr4g  2855  brelrng  5954  elabrex  7261  elabrexg  7262  fliftel1  7329  ovidig  7574  unielxp  8050  tfrlem11  8426  rdglim  8464  seqomlem4  8491  2oconcl  8539  ecopqsi  8812  erov  8852  eroprf  8853  sbthlem2  9122  dffi3  9468  ixpiunwdom  9627  cantnfcl  9704  r1lim  9809  rankwflemb  9830  pwwf  9844  unwf  9847  rankwflem  9852  uniwf  9856  rankpwi  9860  rankr1g  9869  r1pw  9882  r1rankid  9896  rankuni  9900  djulcl  9947  djurcl  9948  inlresf  9951  inrresf  9953  djuun  9963  cardlim  10009  infxpenlem  10050  alephfp  10145  cfsmolem  10307  alephsing  10313  hsmexlem4  10466  axdc3lem2  10488  numth3  10507  iunfo  10576  konigthlem  10605  iunctb  10611  canthwelem  10687  canthwe  10688  r1limwun  10773  inar1  10812  inatsk  10815  gruina  10855  grur1  10857  tskmval  10876  tskmcl  10878  pinq  10964  dmrecnq  11005  addclsr  11120  mulclsr  11121  axaddf  11182  axmulf  11183  peano2nn  12275  uztrn2  12894  eluz2nn  12921  peano2uzs  12941  uzsupss  12979  uzsup  13899  uzrdgfni  13995  uzrdgsuci  13997  fsuppmapnn0fiub  14028  seqf  14060  ser0  14091  bcm1k  14350  bcp1nk  14352  bcpasc  14356  hashprdifel  14433  fz1isolem  14496  pr2pwpr  14514  tpf  14534  ccats1val2  14661  rexuzre  15387  limsupgre  15513  climconst  15575  rlimclim1  15577  climrlim2  15579  clim2ser  15687  clim2ser2  15688  iserex  15689  isermulc2  15690  iserle  15692  isercolllem3  15699  isercoll2  15701  climsup  15702  iseraltlem2  15715  iseraltlem3  15716  zsum  15750  isumclim3  15791  isumadd  15799  fsump1i  15801  iserabs  15847  cvgcmp  15848  cvgcmpub  15849  cvgcmpce  15850  abscvgcvg  15851  isumshft  15871  isumsplit  15872  isum1p  15873  isumrpcl  15875  isumsup2  15878  climcndslem1  15881  cvgrat  15915  clim2prod  15920  clim2div  15921  prodf1  15923  ntrivcvgn0  15930  ntrivcvgtail  15932  fprodntriv  15974  fprodabs  16006  fprodeq0  16007  iprodclim3  16032  iprodmul  16035  ef0lem  16110  fprodefsum  16127  rpnnen2lem3  16248  dvdsflip  16350  fzo0dvdseq  16356  bitsinv1  16475  smupval  16521  smueqlem  16523  seq1st  16604  algr0  16605  prmind2  16718  crth  16811  eulerthlem2  16815  prmdiv  16818  pockthlem  16938  pockthg  16939  unbenlem  16941  prmunb  16947  prmgaplem7  17090  strfv2d  17235  imasvscaval  17584  oppccatid  17765  oppccatf  17774  epii  17790  fthepi  17981  funcestrcsetclem3  18197  funcsetcestrclem3  18211  yon12  18321  yon2  18322  yonedalem4c  18333  yonedalem22  18334  yonedalem3b  18335  yonedainv  18337  acsmapd  18611  mgm2nsgrplem1  18943  mgm2nsgrplem2  18944  mgm2nsgrplem3  18945  sgrp2nmndlem1  18948  sgrp2rid2  18951  ghmqusker  19317  cntrsubgnsg  19373  symgpssefmnd  19427  pmtrrn  19489  gexcl3  19619  efgi  19751  efgi2  19757  efgs1b  19768  efgredlemg  19774  efgredlemd  19776  frgpnabllem1  19905  cycsubgcyg  19933  gsumzaddlem  19953  dprdwd  20045  dprd2da  20076  rhmopp  20525  lsppratlem3  21168  lsppratlem4  21169  lbsextlem2  21178  lidl0ALT  21255  lidl1ALT  21258  2idl0  21287  2idl1  21288  domnchr  21564  znf1o  21587  mplsubrglem  22041  mpfconst  22142  mpfproj  22143  mpfind  22148  mhpmulcl  22170  pf1const  22365  pf1id  22366  mpfpf1  22370  pf1mpf  22371  madetsumid  22482  slesolex  22703  pmatcoe1fsupp  22722  mat2pmatbas0  22748  pmatcollpw  22802  pm2mpf1  22820  isclo  23110  indiscld  23114  restntr  23205  ordtbaslem  23211  ordtbas2  23214  lmconst  23284  lmss  23321  conncompid  23454  2ndcomap  23481  locfincmp  23549  comppfsc  23555  xkouni  23622  txcls  23627  ptclsg  23638  uptx  23648  txindis  23657  tx1stc  23673  cnmpt1res  23699  tgqtop  23735  uffix  23944  cnpflf2  24023  ptcmplem2  24076  ptcmplem4  24078  tgpconncomp  24136  tsmsfbas  24151  fmucnd  24316  prdsxmetlem  24393  imasdsf1olem  24398  prdsbl  24519  blcvx  24833  xrsmopn  24847  xrge0tsms  24869  metdcn2  24874  expcncf  24966  cnmpopc  24968  icchmeo  24984  icchmeoOLD  24985  iccpnfhmeo  24989  cnheibor  25000  evth  25004  evth2  25005  lebnumlem2  25007  lebnumii  25011  reparphti  25042  reparphtiOLD  25043  cfilfcls  25321  minveclem2  25473  minveclem3  25476  minveclem4  25479  ovoliunlem1  25550  ovolicc1  25564  iundisj  25596  volsup  25604  uniioombllem3  25633  vitalilem2  25657  vitalilem3  25658  mbfsup  25712  mbfinf  25713  mbflimsup  25714  itg2monolem1  25799  limcflflem  25929  limccnp  25940  limccnp2  25941  dvidlem  25964  dvn2bss  25980  cpnres  25987  dvcobr  25997  dvcobrOLD  25998  dvrec  26007  c1liplem1  26049  dvcnvrelem2  26071  dvfsumrlimf  26079  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsumrlim  26086  dvfsum2  26089  coeeulem  26277  coeid3  26293  plycn  26314  plycnOLD  26315  dvntaylp  26427  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulm2  26442  ulmshftlem  26446  ulmshft  26447  ulm0  26448  ulmcn  26456  ulmdvlem3  26459  ulmdv  26460  mtest  26461  mtestbdd  26462  dvradcnv  26478  psercn2  26480  psercn2OLD  26481  psercn  26484  pserdv  26487  abelth  26499  efif1olem2  26599  efif1olem4  26601  efifo  26603  eff1olem  26604  logcn  26703  dvloglem  26704  cxpcn3  26805  resqrtcn  26806  sqrtcn  26807  logbleb  26840  logblt  26841  asinneg  26943  atanlogsub  26973  atanbnd  26983  ressatans  26991  leibpilem2  26998  xrlimcnp  27025  efrlim  27026  efrlimOLD  27027  scvxcvx  27043  ppiub  27262  chtub  27270  logexprlim  27283  lgseisenlem1  27433  rplogsumlem1  27542  rplogsumlem2  27543  dchrisumlem2  27548  dchrisum0flb  27568  logdivbnd  27614  pntlem3  27667  dfnns2  28376  tgcgr4  28553  ltgov  28619  f1otrg  28893  eengtrkg  29015  iedgedg  29081  ushgredgedgloop  29262  subgruhgredgd  29315  uvtxupgrres  29439  umgr2v2evd2  29559  edginwlk  29667  wlk1walk  29671  crctcshwlkn0lem6  29844  wlkiswwlks1  29896  minvecolem1  30902  minvecolem2  30903  minvecolem4  30908  htthlem  30945  5oalem2  31683  3oalem2  31691  iundisjf  32608  fmptco1f1o  32649  xppreima  32661  xppreima2  32667  dfcnv2  32692  ccatws1f1o  32920  chnub  32985  gsumhashmul  33046  xrge0tsmsd  33047  gsumwrd2dccatlem  33051  odpmco  33088  pmtrcnelor  33093  fzo0pmtrlast  33094  wrdpmtrlast  33095  pmtrto1cl  33101  psgnfzto1stlem  33102  fzto1stfv1  33103  fzto1st  33105  fzto1stinvn  33106  psgnfzto1st  33107  tocycf  33119  cycpmco2lem7  33134  cycpmco2  33135  cycpmrn  33145  cyc3evpm  33152  cyc3genpmlem  33153  cycpmgcl  33155  cyc3conja  33159  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  nsgmgc  33419  nsgqusf1olem1  33420  nsgqusf1olem2  33421  rhmpreimaprmidl  33458  ssdifidllem  33463  ssdifidl  33464  ssmxidllem  33480  drngmxidlr  33485  opprqus1r  33499  qsdrngilem  33501  qsdrngi  33502  rsprprmprmidlb  33530  rprmirredb  33539  1arithufdlem1  33551  1arithufdlem2  33552  1arithufdlem3  33553  1arithufdlem4  33554  fply1  33563  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  ply1degltdimlem  33649  ply1degltdim  33650  algextdeglem4  33725  algextdeglem6  33727  algextdeglem7  33728  algextdeglem8  33729  smatlem  33757  smatcl  33762  zartopn  33835  zarmxt1  33840  tpr2rico  33872  xrmulc1cn  33890  xrge0mulc1cn  33901  esumpfinvallem  34054  ldgenpisyslem1  34143  dynkin  34147  brfae  34228  sxbrsigalem3  34253  dya2icoseg2  34259  omsmeas  34304  sibfof  34321  sseqmw  34372  sseqf  34373  sseqp1  34376  fiblem  34379  fibp1  34382  probfinmeasbALTV  34410  repr0  34604  reprpmtf1o  34619  hgt750lemg  34647  bnj1379  34822  srcmpltd  35072  subfacp1lem5  35168  subfacp1lem6  35169  cvxpconn  35226  cvxsconn  35227  cvmliftlem6  35274  cvmliftlem8  35276  cvmliftlem10  35278  cvmlift2lem6  35292  cvmlift2lem11  35297  cvmlift2lem12  35298  2goelgoanfmla1  35408  prv1n  35415  msubff  35514  msubco  35515  elmsta  35532  msubff1  35540  mvhf  35542  msubvrs  35544  iprodefisumlem  35719  filnetlem3  36362  knoppcnlem10  36484  knoppcnlem11  36485  icoreunrn  37341  icoreelrn  37343  ralssiun  37389  poimirlem3  37609  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem30  37636  dvasin  37690  cover2  37701  upixp  37715  sdclem1  37729  fdc  37731  caushft  37747  ismtyres  37794  rrncmslem  37818  isfld2  37991  osumcllem10N  39947  pexmidlem7N  39958  dihglblem2N  41276  lcfrvalsnN  41523  lcfrlem5  41528  lcfrlem6  41529  lcfrlem27  41551  lcfrlem37  41561  aks6d1c1p4  42092  aks6d1c1p7  42094  aks6d1c1p8  42096  evl1gprodd  42098  aks6d1c2lem4  42108  aks6d1c5lem3  42118  aks6d1c6lem2  42152  prjspvs  42596  0prjspnrel  42613  monotuz  42929  expdiophlem1  43009  kelac2  43053  naddwordnexlem4  43390  grurankcld  44228  dvgrat  44307  nzss  44312  uzmptshftfval  44341  binomcxplemnotnn0  44351  refsumcn  44967  rfcnpre2  44968  rfcnpre3  44970  rfcnpre4  44971  disjf1o  45133  unirnmap  45150  unirnmapsn  45156  ssmapsn  45158  mptssid  45184  allbutfi  45342  eluzd  45358  uzidd2  45365  ressiocsup  45506  ressioosup  45507  ressiooinf  45509  fsumsermpt  45534  climexp  45560  climinf  45561  climsuse  45563  sumnnodd  45585  limsupresico  45655  limsupubuzlem  45667  limsupresxr  45721  liminfresxr  45722  liminfresico  45726  limsup10exlem  45727  cnrefiisplem  45784  cncfiooicclem1  45848  dvsinax  45868  itgsinexplem1  45909  fvvolioof  45944  fvvolicof  45946  stoweidlem14  45969  stoweidlem16  45971  stoweidlem31  45986  stoweidlem34  45989  stoweidlem36  45991  stoweidlem43  45998  stoweidlem46  46001  stoweidlem47  46002  stoweidlem52  46007  stoweidlem55  46010  stoweidlem57  46012  dirkercncf  46062  fourierdlem20  46082  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem51  46112  fourierdlem54  46115  fourierdlem62  46123  fourierdlem71  46132  fourierdlem80  46141  fourierdlem114  46175  fouriersw  46186  ioorrnopnlem  46259  ioorrnopnxrlem  46261  salexct3  46297  salgencntex  46298  salgensscntex  46299  subsalsal  46314  sge0fodjrnlem  46371  sge0isum  46382  sge0seq  46401  sge0reuz  46402  sge0reuzb  46403  meadjiunlem  46420  meaiininclem  46441  carageniuncllem1  46476  caratheodorylem1  46481  hoiprodp1  46543  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  voncmpl  46576  hoiqssbl  46580  smflimlem2  46727  smfsuplem1  46766  smfsuplem3  46768  fsupdm  46797  finfdm  46801  cfsetsnfsetf  47007  fcores  47016  afvres  47121  afv2res  47188  fundcmpsurinjimaid  47335  iccpartigtl  47347  sprsymrelf  47419  prproropf1olem2  47428  isuspgrim0lem  47808  isuspgrimlem  47811  ushggricedg  47833  grimedg  47840  usgrgrtrirex  47852  isubgr3stgrlem7  47874  uspgrlimlem4  47893  gpgedgel  47942  funcringcsetcALTV2lem3  48135  funcringcsetclem3ALTV  48158  lindslinindsimp2lem5  48307  rrxsphere  48597  line2  48601  iooii  48713  icccldii  48714  iscnrm3rlem3  48738  onsetreclem3  48937  amgmwlem  49032