Theorem eleqtrrdi 2845

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 2844	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

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

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 2115  ax-9 2123  ax-ext 2706

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

This theorem is referenced by:  3eltr4g  2851  brelrng  5888  elabrex  7186  elabrexg  7187  fliftel1  7254  ovidig  7498  unielxp  7969  tfrlem11  8317  rdglim  8355  seqomlem4  8382  2oconcl  8428  ecopqsi  8706  erov  8749  eroprf  8750  sbthlem2  9014  dffi3  9332  ixpiunwdom  9493  cantnfcl  9574  r1lim  9682  rankwflemb  9703  pwwf  9717  unwf  9720  rankwflem  9725  uniwf  9729  rankpwi  9733  rankr1g  9742  r1pw  9755  r1rankid  9769  rankuni  9773  djulcl  9820  djurcl  9821  inlresf  9824  inrresf  9826  djuun  9836  cardlim  9882  infxpenlem  9921  alephfp  10016  cfsmolem  10178  alephsing  10184  hsmexlem4  10337  axdc3lem2  10359  numth3  10378  iunfo  10447  konigthlem  10477  iunctb  10483  canthwelem  10559  canthwe  10560  r1limwun  10645  inar1  10684  inatsk  10687  gruina  10727  grur1  10729  tskmval  10748  tskmcl  10750  pinq  10836  dmrecnq  10877  addclsr  10992  mulclsr  10993  axaddf  11054  axmulf  11055  peano2nn  12155  uztrn2  12768  eluz2nn  12799  peano2uzs  12813  uzsupss  12851  uzsup  13781  uzrdgfni  13879  uzrdgsuci  13881  fsuppmapnn0fiub  13912  seqf  13944  ser0  13975  bcm1k  14236  bcp1nk  14238  bcpasc  14242  hashprdifel  14319  fz1isolem  14382  pr2pwpr  14400  tpf  14420  ccats1val2  14549  rexuzre  15274  limsupgre  15402  climconst  15464  rlimclim1  15466  climrlim2  15468  clim2ser  15576  clim2ser2  15577  iserex  15578  isermulc2  15579  iserle  15581  isercolllem3  15588  isercoll2  15590  climsup  15591  iseraltlem2  15604  iseraltlem3  15605  zsum  15639  isumclim3  15680  isumadd  15688  fsump1i  15690  iserabs  15736  cvgcmp  15737  cvgcmpub  15738  cvgcmpce  15739  abscvgcvg  15740  isumshft  15760  isumsplit  15761  isum1p  15762  isumrpcl  15764  isumsup2  15767  climcndslem1  15770  cvgrat  15804  clim2prod  15809  clim2div  15810  prodf1  15812  ntrivcvgn0  15819  ntrivcvgtail  15821  fprodntriv  15863  fprodabs  15895  fprodeq0  15896  iprodclim3  15921  iprodmul  15924  ef0lem  15999  fprodefsum  16016  rpnnen2lem3  16139  dvdsflip  16242  fzo0dvdseq  16248  bitsinv1  16367  smupval  16413  smueqlem  16415  seq1st  16496  algr0  16497  prmind2  16610  crth  16703  eulerthlem2  16707  prmdiv  16710  pockthlem  16831  pockthg  16832  unbenlem  16834  prmunb  16840  prmgaplem7  16983  strfv2d  17126  imasvscaval  17457  oppccatid  17640  oppccatf  17649  epii  17665  fthepi  17852  funcestrcsetclem3  18063  funcsetcestrclem3  18077  yon12  18186  yon2  18187  yonedalem4c  18198  yonedalem22  18199  yonedalem3b  18200  yonedainv  18202  acsmapd  18475  chnub  18543  chnccats1  18546  chnccat  18547  mgm2nsgrplem1  18841  mgm2nsgrplem2  18842  mgm2nsgrplem3  18843  sgrp2nmndlem1  18846  sgrp2rid2  18849  ghmqusker  19214  cntrsubgnsg  19270  symgpssefmnd  19323  pmtrrn  19384  gexcl3  19514  efgi  19646  efgi2  19652  efgs1b  19663  efgredlemg  19669  efgredlemd  19671  frgpnabllem1  19800  cycsubgcyg  19828  gsumzaddlem  19848  dprdwd  19940  dprd2da  19971  rhmopp  20440  lsppratlem3  21102  lsppratlem4  21103  lbsextlem2  21112  lidl0ALT  21181  lidl1ALT  21184  2idl0  21213  2idl1  21214  domnchr  21485  znf1o  21504  mplsubrglem  21957  mpfconst  22062  mpfproj  22063  mpfind  22068  mhpmulcl  22090  pf1const  22288  pf1id  22289  mpfpf1  22293  pf1mpf  22294  madetsumid  22403  slesolex  22624  pmatcoe1fsupp  22643  mat2pmatbas0  22669  pmatcollpw  22723  pm2mpf1  22741  isclo  23029  indiscld  23033  restntr  23124  ordtbaslem  23130  ordtbas2  23133  lmconst  23203  lmss  23240  conncompid  23373  2ndcomap  23400  locfincmp  23468  comppfsc  23474  xkouni  23541  txcls  23546  ptclsg  23557  uptx  23567  txindis  23576  tx1stc  23592  cnmpt1res  23618  tgqtop  23654  uffix  23863  cnpflf2  23942  ptcmplem2  23995  ptcmplem4  23997  tgpconncomp  24055  tsmsfbas  24070  fmucnd  24233  prdsxmetlem  24310  imasdsf1olem  24315  prdsbl  24433  blcvx  24740  xrsmopn  24755  xrge0tsms  24777  metdcn2  24782  expcncf  24874  cnmpopc  24876  icchmeo  24892  icchmeoOLD  24893  iccpnfhmeo  24897  cnheibor  24908  evth  24912  evth2  24913  lebnumlem2  24915  lebnumii  24919  reparphti  24950  reparphtiOLD  24951  cfilfcls  25228  minveclem2  25380  minveclem3  25383  minveclem4  25386  ovoliunlem1  25457  ovolicc1  25471  iundisj  25503  volsup  25511  uniioombllem3  25540  vitalilem2  25564  vitalilem3  25565  mbfsup  25619  mbfinf  25620  mbflimsup  25621  itg2monolem1  25705  limcflflem  25835  limccnp  25846  limccnp2  25847  dvidlem  25870  dvn2bss  25886  cpnres  25893  dvcobr  25903  dvcobrOLD  25904  dvrec  25913  c1liplem1  25955  dvcnvrelem2  25977  dvfsumrlimf  25985  dvfsumlem1  25986  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumlem3  25989  dvfsumlem4  25990  dvfsumrlim  25992  dvfsum2  25995  coeeulem  26183  coeid3  26199  plycn  26220  plycnOLD  26221  dvntaylp  26333  taylthlem1  26335  taylthlem2  26336  taylthlem2OLD  26337  ulm2  26348  ulmshftlem  26352  ulmshft  26353  ulm0  26354  ulmcn  26362  ulmdvlem3  26365  ulmdv  26366  mtest  26367  mtestbdd  26368  dvradcnv  26384  psercn2  26386  psercn2OLD  26387  psercn  26390  pserdv  26393  abelth  26405  efif1olem2  26506  efif1olem4  26508  efifo  26510  eff1olem  26511  logcn  26610  dvloglem  26611  cxpcn3  26712  resqrtcn  26713  sqrtcn  26714  logbleb  26747  logblt  26748  asinneg  26850  atanlogsub  26880  atanbnd  26890  ressatans  26898  leibpilem2  26905  xrlimcnp  26932  efrlim  26933  efrlimOLD  26934  scvxcvx  26950  ppiub  27169  chtub  27177  logexprlim  27190  lgseisenlem1  27340  rplogsumlem1  27449  rplogsumlem2  27450  dchrisumlem2  27455  dchrisum0flb  27475  logdivbnd  27521  pntlem3  27574  dfnns2  28330  tgcgr4  28552  ltgov  28618  f1otrg  28892  eengtrkg  29008  iedgedg  29072  ushgredgedgloop  29253  subgruhgredgd  29306  uvtxupgrres  29430  umgr2v2evd2  29550  edginwlk  29657  wlk1walk  29661  crctcshwlkn0lem6  29837  wlkiswwlks1  29889  minvecolem1  30898  minvecolem2  30899  minvecolem4  30904  htthlem  30941  5oalem2  31679  3oalem2  31687  iundisjf  32613  fmptco1f1o  32660  xppreima  32672  xppreima2  32678  dfcnv2  32703  ccatws1f1o  32982  gsumhashmul  33099  xrge0tsmsd  33104  gsumwrd2dccatlem  33108  odpmco  33117  pmtrcnelor  33122  fzo0pmtrlast  33123  wrdpmtrlast  33124  pmtrto1cl  33130  psgnfzto1stlem  33131  fzto1stfv1  33132  fzto1st  33134  fzto1stinvn  33135  psgnfzto1st  33136  tocycf  33148  cycpmco2lem7  33163  cycpmco2  33164  cycpmrn  33174  cyc3evpm  33181  cyc3genpmlem  33182  cycpmgcl  33184  cyc3conja  33188  elrgspnlem1  33273  elrgspnlem2  33274  elrgspnlem3  33275  elrgspnlem4  33276  elrgspnsubrunlem1  33278  nsgmgc  33442  nsgqusf1olem1  33443  nsgqusf1olem2  33444  rhmpreimaprmidl  33481  ssdifidllem  33486  ssdifidl  33487  ssmxidllem  33503  drngmxidlr  33508  opprqus1r  33522  qsdrngilem  33524  qsdrngi  33525  rsprprmprmidlb  33553  rprmirredb  33562  1arithufdlem1  33574  1arithufdlem2  33575  1arithufdlem3  33576  1arithufdlem4  33577  fply1  33588  ply1degltel  33624  ply1degleel  33625  ply1degltlss  33626  mplmulmvr  33653  esplylem  33673  esplyfv1  33676  esplysply  33678  esplyind  33680  ply1degltdimlem  33728  ply1degltdim  33729  algextdeglem4  33826  algextdeglem6  33828  algextdeglem7  33829  algextdeglem8  33830  nn0constr  33867  smatlem  33903  smatcl  33908  zartopn  33981  zarmxt1  33986  tpr2rico  34018  xrmulc1cn  34036  xrge0mulc1cn  34047  esumpfinvallem  34180  ldgenpisyslem1  34269  dynkin  34273  brfae  34354  sxbrsigalem3  34378  dya2icoseg2  34384  omsmeas  34429  sibfof  34446  sseqmw  34497  sseqf  34498  sseqp1  34501  fiblem  34504  fibp1  34507  probfinmeasbALTV  34535  repr0  34717  reprpmtf1o  34732  hgt750lemg  34760  bnj1379  34935  srcmpltd  35185  fineqvnttrclselem3  35228  subfacp1lem5  35327  subfacp1lem6  35328  cvxpconn  35385  cvxsconn  35386  cvmliftlem6  35433  cvmliftlem8  35435  cvmliftlem10  35437  cvmlift2lem6  35451  cvmlift2lem11  35456  cvmlift2lem12  35457  2goelgoanfmla1  35567  prv1n  35574  msubff  35673  msubco  35674  elmsta  35691  msubff1  35699  mvhf  35701  msubvrs  35703  iprodefisumlem  35883  filnetlem3  36523  knoppcnlem10  36645  knoppcnlem11  36646  icoreunrn  37503  icoreelrn  37505  ralssiun  37551  poimirlem3  37763  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem30  37790  dvasin  37844  cover2  37855  upixp  37869  sdclem1  37883  fdc  37885  caushft  37901  ismtyres  37948  rrncmslem  37972  isfld2  38145  presuc  38610  osumcllem10N  40164  pexmidlem7N  40175  dihglblem2N  41493  lcfrvalsnN  41740  lcfrlem5  41745  lcfrlem6  41746  lcfrlem27  41768  lcfrlem37  41778  aks6d1c1p4  42304  aks6d1c1p7  42306  aks6d1c1p8  42308  evl1gprodd  42310  aks6d1c2lem4  42320  aks6d1c5lem3  42330  aks6d1c6lem2  42364  prjspvs  42795  0prjspnrel  42812  monotuz  43125  expdiophlem1  43205  kelac2  43249  naddwordnexlem4  43585  grurankcld  44416  dvgrat  44495  nzss  44500  uzmptshftfval  44529  binomcxplemnotnn0  44539  orbitinit  45139  orbitcl  45140  permaxinf2lem  45195  refsumcn  45217  rfcnpre2  45218  rfcnpre3  45220  rfcnpre4  45221  disjf1o  45377  unirnmap  45394  unirnmapsn  45400  ssmapsn  45402  mptssid  45427  allbutfi  45579  eluzd  45595  uzidd2  45602  ressiocsup  45742  ressioosup  45743  ressiooinf  45745  fsumsermpt  45767  climexp  45793  climinf  45794  climsuse  45796  sumnnodd  45818  limsupresico  45886  limsupubuzlem  45898  limsupresxr  45952  liminfresxr  45953  liminfresico  45957  limsup10exlem  45958  cnrefiisplem  46015  cncfiooicclem1  46079  dvsinax  46099  itgsinexplem1  46140  fvvolioof  46175  fvvolicof  46177  stoweidlem14  46200  stoweidlem16  46202  stoweidlem31  46217  stoweidlem34  46220  stoweidlem36  46222  stoweidlem43  46229  stoweidlem46  46232  stoweidlem47  46233  stoweidlem52  46238  stoweidlem55  46241  stoweidlem57  46243  dirkercncf  46293  fourierdlem20  46313  fourierdlem42  46335  fourierdlem48  46340  fourierdlem49  46341  fourierdlem51  46343  fourierdlem54  46346  fourierdlem62  46354  fourierdlem71  46363  fourierdlem80  46372  fourierdlem114  46406  fouriersw  46417  ioorrnopnlem  46490  ioorrnopnxrlem  46492  salexct3  46528  salgencntex  46529  salgensscntex  46530  subsalsal  46545  sge0fodjrnlem  46602  sge0isum  46613  sge0seq  46632  sge0reuz  46633  sge0reuzb  46634  meadjiunlem  46651  meaiininclem  46672  carageniuncllem1  46707  caratheodorylem1  46712  hoiprodp1  46774  hoidmv1lelem1  46777  hoidmv1lelem2  46778  hoidmv1le  46780  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem3  46783  voncmpl  46807  hoiqssbl  46811  smflimlem2  46958  smfsuplem1  46997  smfsuplem3  46999  fsupdm  47028  finfdm  47032  cfsetsnfsetf  47246  fcores  47255  afvres  47360  afv2res  47427  fundcmpsurinjimaid  47599  iccpartigtl  47611  sprsymrelf  47683  prproropf1olem2  47692  uhgrimedgi  48078  isuspgrim0lem  48081  isuspgrimlem  48083  ushggricedg  48115  grimedg  48123  usgrgrtrirex  48138  isubgr3stgrlem7  48160  uspgrlimlem4  48179  grlimprclnbgr  48184  gpgiedgdmellem  48234  gpg3kgrtriex  48277  funcringcsetcALTV2lem3  48480  funcringcsetclem3ALTV  48503  lindslinindsimp2lem5  48650  rrxsphere  48936  line2  48940  iooii  49105  icccldii  49106  iscnrm3rlem3  49129  eloppf2  49321  oppcup  49394  natoppf  49416  zeroo2  49421  oppfdiag1  49601  oppfdiag  49603  2arwcat  49787  incat  49788  lmddu  49854  onsetreclem3  49894  amgmwlem  49989