Theorem eleqtrrdi 2840

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804

This theorem is referenced by:  3eltr4g  2846  brelrng  5907  elabrex  7218  elabrexg  7219  fliftel1  7287  ovidig  7533  unielxp  8008  tfrlem11  8358  rdglim  8396  seqomlem4  8423  2oconcl  8469  ecopqsi  8746  erov  8789  eroprf  8790  sbthlem2  9057  dffi3  9388  ixpiunwdom  9549  cantnfcl  9626  r1lim  9731  rankwflemb  9752  pwwf  9766  unwf  9769  rankwflem  9774  uniwf  9778  rankpwi  9782  rankr1g  9791  r1pw  9804  r1rankid  9818  rankuni  9822  djulcl  9869  djurcl  9870  inlresf  9873  inrresf  9875  djuun  9885  cardlim  9931  infxpenlem  9972  alephfp  10067  cfsmolem  10229  alephsing  10235  hsmexlem4  10388  axdc3lem2  10410  numth3  10429  iunfo  10498  konigthlem  10527  iunctb  10533  canthwelem  10609  canthwe  10610  r1limwun  10695  inar1  10734  inatsk  10737  gruina  10777  grur1  10779  tskmval  10798  tskmcl  10800  pinq  10886  dmrecnq  10927  addclsr  11042  mulclsr  11043  axaddf  11104  axmulf  11105  peano2nn  12199  uztrn2  12818  eluz2nn  12853  peano2uzs  12867  uzsupss  12905  uzsup  13831  uzrdgfni  13929  uzrdgsuci  13931  fsuppmapnn0fiub  13962  seqf  13994  ser0  14025  bcm1k  14286  bcp1nk  14288  bcpasc  14292  hashprdifel  14369  fz1isolem  14432  pr2pwpr  14450  tpf  14470  ccats1val2  14598  rexuzre  15325  limsupgre  15453  climconst  15515  rlimclim1  15517  climrlim2  15519  clim2ser  15627  clim2ser2  15628  iserex  15629  isermulc2  15630  iserle  15632  isercolllem3  15639  isercoll2  15641  climsup  15642  iseraltlem2  15655  iseraltlem3  15656  zsum  15690  isumclim3  15731  isumadd  15739  fsump1i  15741  iserabs  15787  cvgcmp  15788  cvgcmpub  15789  cvgcmpce  15790  abscvgcvg  15791  isumshft  15811  isumsplit  15812  isum1p  15813  isumrpcl  15815  isumsup2  15818  climcndslem1  15821  cvgrat  15855  clim2prod  15860  clim2div  15861  prodf1  15863  ntrivcvgn0  15870  ntrivcvgtail  15872  fprodntriv  15914  fprodabs  15946  fprodeq0  15947  iprodclim3  15972  iprodmul  15975  ef0lem  16050  fprodefsum  16067  rpnnen2lem3  16190  dvdsflip  16293  fzo0dvdseq  16299  bitsinv1  16418  smupval  16464  smueqlem  16466  seq1st  16547  algr0  16548  prmind2  16661  crth  16754  eulerthlem2  16758  prmdiv  16761  pockthlem  16882  pockthg  16883  unbenlem  16885  prmunb  16891  prmgaplem7  17034  strfv2d  17177  imasvscaval  17507  oppccatid  17686  oppccatf  17695  epii  17711  fthepi  17898  funcestrcsetclem3  18109  funcsetcestrclem3  18123  yon12  18232  yon2  18233  yonedalem4c  18244  yonedalem22  18245  yonedalem3b  18246  yonedainv  18248  acsmapd  18519  mgm2nsgrplem1  18851  mgm2nsgrplem2  18852  mgm2nsgrplem3  18853  sgrp2nmndlem1  18856  sgrp2rid2  18859  ghmqusker  19225  cntrsubgnsg  19281  symgpssefmnd  19332  pmtrrn  19393  gexcl3  19523  efgi  19655  efgi2  19661  efgs1b  19672  efgredlemg  19678  efgredlemd  19680  frgpnabllem1  19809  cycsubgcyg  19837  gsumzaddlem  19857  dprdwd  19949  dprd2da  19980  rhmopp  20424  lsppratlem3  21065  lsppratlem4  21066  lbsextlem2  21075  lidl0ALT  21144  lidl1ALT  21147  2idl0  21176  2idl1  21177  domnchr  21448  znf1o  21467  mplsubrglem  21919  mpfconst  22014  mpfproj  22015  mpfind  22020  mhpmulcl  22042  pf1const  22239  pf1id  22240  mpfpf1  22244  pf1mpf  22245  madetsumid  22354  slesolex  22575  pmatcoe1fsupp  22594  mat2pmatbas0  22620  pmatcollpw  22674  pm2mpf1  22692  isclo  22980  indiscld  22984  restntr  23075  ordtbaslem  23081  ordtbas2  23084  lmconst  23154  lmss  23191  conncompid  23324  2ndcomap  23351  locfincmp  23419  comppfsc  23425  xkouni  23492  txcls  23497  ptclsg  23508  uptx  23518  txindis  23527  tx1stc  23543  cnmpt1res  23569  tgqtop  23605  uffix  23814  cnpflf2  23893  ptcmplem2  23946  ptcmplem4  23948  tgpconncomp  24006  tsmsfbas  24021  fmucnd  24185  prdsxmetlem  24262  imasdsf1olem  24267  prdsbl  24385  blcvx  24692  xrsmopn  24707  xrge0tsms  24729  metdcn2  24734  expcncf  24826  cnmpopc  24828  icchmeo  24844  icchmeoOLD  24845  iccpnfhmeo  24849  cnheibor  24860  evth  24864  evth2  24865  lebnumlem2  24867  lebnumii  24871  reparphti  24902  reparphtiOLD  24903  cfilfcls  25180  minveclem2  25332  minveclem3  25335  minveclem4  25338  ovoliunlem1  25409  ovolicc1  25423  iundisj  25455  volsup  25463  uniioombllem3  25492  vitalilem2  25516  vitalilem3  25517  mbfsup  25571  mbfinf  25572  mbflimsup  25573  itg2monolem1  25657  limcflflem  25787  limccnp  25798  limccnp2  25799  dvidlem  25822  dvn2bss  25838  cpnres  25845  dvcobr  25855  dvcobrOLD  25856  dvrec  25865  c1liplem1  25907  dvcnvrelem2  25929  dvfsumrlimf  25937  dvfsumlem1  25938  dvfsumlem2  25939  dvfsumlem2OLD  25940  dvfsumlem3  25941  dvfsumlem4  25942  dvfsumrlim  25944  dvfsum2  25947  coeeulem  26135  coeid3  26151  plycn  26172  plycnOLD  26173  dvntaylp  26285  taylthlem1  26287  taylthlem2  26288  taylthlem2OLD  26289  ulm2  26300  ulmshftlem  26304  ulmshft  26305  ulm0  26306  ulmcn  26314  ulmdvlem3  26317  ulmdv  26318  mtest  26319  mtestbdd  26320  dvradcnv  26336  psercn2  26338  psercn2OLD  26339  psercn  26342  pserdv  26345  abelth  26357  efif1olem2  26458  efif1olem4  26460  efifo  26462  eff1olem  26463  logcn  26562  dvloglem  26563  cxpcn3  26664  resqrtcn  26665  sqrtcn  26666  logbleb  26699  logblt  26700  asinneg  26802  atanlogsub  26832  atanbnd  26842  ressatans  26850  leibpilem2  26857  xrlimcnp  26884  efrlim  26885  efrlimOLD  26886  scvxcvx  26902  ppiub  27121  chtub  27129  logexprlim  27142  lgseisenlem1  27292  rplogsumlem1  27401  rplogsumlem2  27402  dchrisumlem2  27407  dchrisum0flb  27427  logdivbnd  27473  pntlem3  27526  dfnns2  28267  tgcgr4  28464  ltgov  28530  f1otrg  28804  eengtrkg  28919  iedgedg  28983  ushgredgedgloop  29164  subgruhgredgd  29217  uvtxupgrres  29341  umgr2v2evd2  29461  edginwlk  29569  wlk1walk  29573  crctcshwlkn0lem6  29751  wlkiswwlks1  29803  minvecolem1  30809  minvecolem2  30810  minvecolem4  30815  htthlem  30852  5oalem2  31590  3oalem2  31598  iundisjf  32524  fmptco1f1o  32563  xppreima  32575  xppreima2  32581  dfcnv2  32606  ccatws1f1o  32879  chnub  32944  chnccats1  32947  gsumhashmul  33007  xrge0tsmsd  33008  gsumwrd2dccatlem  33012  odpmco  33049  pmtrcnelor  33054  fzo0pmtrlast  33055  wrdpmtrlast  33056  pmtrto1cl  33062  psgnfzto1stlem  33063  fzto1stfv1  33064  fzto1st  33066  fzto1stinvn  33067  psgnfzto1st  33068  tocycf  33080  cycpmco2lem7  33095  cycpmco2  33096  cycpmrn  33106  cyc3evpm  33113  cyc3genpmlem  33114  cycpmgcl  33116  cyc3conja  33120  elrgspnlem1  33199  elrgspnlem2  33200  elrgspnlem3  33201  elrgspnlem4  33202  elrgspnsubrunlem1  33204  nsgmgc  33389  nsgqusf1olem1  33390  nsgqusf1olem2  33391  rhmpreimaprmidl  33428  ssdifidllem  33433  ssdifidl  33434  ssmxidllem  33450  drngmxidlr  33455  opprqus1r  33469  qsdrngilem  33471  qsdrngi  33472  rsprprmprmidlb  33500  rprmirredb  33509  1arithufdlem1  33521  1arithufdlem2  33522  1arithufdlem3  33523  1arithufdlem4  33524  fply1  33533  ply1degltel  33566  ply1degleel  33567  ply1degltlss  33568  ply1degltdimlem  33624  ply1degltdim  33625  algextdeglem4  33716  algextdeglem6  33718  algextdeglem7  33719  algextdeglem8  33720  nn0constr  33757  smatlem  33793  smatcl  33798  zartopn  33871  zarmxt1  33876  tpr2rico  33908  xrmulc1cn  33926  xrge0mulc1cn  33937  esumpfinvallem  34070  ldgenpisyslem1  34159  dynkin  34163  brfae  34244  sxbrsigalem3  34269  dya2icoseg2  34275  omsmeas  34320  sibfof  34337  sseqmw  34388  sseqf  34389  sseqp1  34392  fiblem  34395  fibp1  34398  probfinmeasbALTV  34426  repr0  34608  reprpmtf1o  34623  hgt750lemg  34651  bnj1379  34826  srcmpltd  35076  subfacp1lem5  35171  subfacp1lem6  35172  cvxpconn  35229  cvxsconn  35230  cvmliftlem6  35277  cvmliftlem8  35279  cvmliftlem10  35281  cvmlift2lem6  35295  cvmlift2lem11  35300  cvmlift2lem12  35301  2goelgoanfmla1  35411  prv1n  35418  msubff  35517  msubco  35518  elmsta  35535  msubff1  35543  mvhf  35545  msubvrs  35547  iprodefisumlem  35722  filnetlem3  36363  knoppcnlem10  36485  knoppcnlem11  36486  icoreunrn  37342  icoreelrn  37344  ralssiun  37390  poimirlem3  37612  poimirlem16  37625  poimirlem17  37626  poimirlem19  37628  poimirlem30  37639  dvasin  37693  cover2  37704  upixp  37718  sdclem1  37732  fdc  37734  caushft  37750  ismtyres  37797  rrncmslem  37821  isfld2  37994  osumcllem10N  39954  pexmidlem7N  39965  dihglblem2N  41283  lcfrvalsnN  41530  lcfrlem5  41535  lcfrlem6  41536  lcfrlem27  41558  lcfrlem37  41568  aks6d1c1p4  42094  aks6d1c1p7  42096  aks6d1c1p8  42098  evl1gprodd  42100  aks6d1c2lem4  42110  aks6d1c5lem3  42120  aks6d1c6lem2  42154  prjspvs  42591  0prjspnrel  42608  monotuz  42923  expdiophlem1  43003  kelac2  43047  naddwordnexlem4  43383  grurankcld  44215  dvgrat  44294  nzss  44299  uzmptshftfval  44328  binomcxplemnotnn0  44338  orbitinit  44939  orbitcl  44940  permaxinf2lem  44995  refsumcn  45017  rfcnpre2  45018  rfcnpre3  45020  rfcnpre4  45021  disjf1o  45178  unirnmap  45195  unirnmapsn  45201  ssmapsn  45203  mptssid  45228  allbutfi  45382  eluzd  45398  uzidd2  45405  ressiocsup  45545  ressioosup  45546  ressiooinf  45548  fsumsermpt  45570  climexp  45596  climinf  45597  climsuse  45599  sumnnodd  45621  limsupresico  45691  limsupubuzlem  45703  limsupresxr  45757  liminfresxr  45758  liminfresico  45762  limsup10exlem  45763  cnrefiisplem  45820  cncfiooicclem1  45884  dvsinax  45904  itgsinexplem1  45945  fvvolioof  45980  fvvolicof  45982  stoweidlem14  46005  stoweidlem16  46007  stoweidlem31  46022  stoweidlem34  46025  stoweidlem36  46027  stoweidlem43  46034  stoweidlem46  46037  stoweidlem47  46038  stoweidlem52  46043  stoweidlem55  46046  stoweidlem57  46048  dirkercncf  46098  fourierdlem20  46118  fourierdlem42  46140  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem54  46151  fourierdlem62  46159  fourierdlem71  46168  fourierdlem80  46177  fourierdlem114  46211  fouriersw  46222  ioorrnopnlem  46295  ioorrnopnxrlem  46297  salexct3  46333  salgencntex  46334  salgensscntex  46335  subsalsal  46350  sge0fodjrnlem  46407  sge0isum  46418  sge0seq  46437  sge0reuz  46438  sge0reuzb  46439  meadjiunlem  46456  meaiininclem  46477  carageniuncllem1  46512  caratheodorylem1  46517  hoiprodp1  46579  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1le  46585  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  voncmpl  46612  hoiqssbl  46616  smflimlem2  46763  smfsuplem1  46802  smfsuplem3  46804  fsupdm  46833  finfdm  46837  cfsetsnfsetf  47049  fcores  47058  afvres  47163  afv2res  47230  fundcmpsurinjimaid  47402  iccpartigtl  47414  sprsymrelf  47486  prproropf1olem2  47495  uhgrimedgi  47880  isuspgrim0lem  47883  isuspgrimlem  47885  ushggricedg  47917  grimedg  47925  usgrgrtrirex  47939  isubgr3stgrlem7  47961  uspgrlimlem4  47980  gpgiedgdmellem  48027  gpg3kgrtriex  48070  funcringcsetcALTV2lem3  48270  funcringcsetclem3ALTV  48293  lindslinindsimp2lem5  48441  rrxsphere  48727  line2  48731  iooii  48896  icccldii  48897  iscnrm3rlem3  48920  eloppf2  49113  oppcup  49186  natoppf  49208  zeroo2  49213  oppfdiag1  49393  oppfdiag  49395  2arwcat  49579  incat  49580  lmddu  49646  onsetreclem3  49686  amgmwlem  49781