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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  3eltr4g  2851  brelrng  5921  elabrex  7233  elabrexg  7234  fliftel1  7302  ovidig  7547  unielxp  8024  tfrlem11  8400  rdglim  8438  seqomlem4  8465  2oconcl  8513  ecopqsi  8786  erov  8826  eroprf  8827  sbthlem2  9096  dffi3  9441  ixpiunwdom  9602  cantnfcl  9679  r1lim  9784  rankwflemb  9805  pwwf  9819  unwf  9822  rankwflem  9827  uniwf  9831  rankpwi  9835  rankr1g  9844  r1pw  9857  r1rankid  9871  rankuni  9875  djulcl  9922  djurcl  9923  inlresf  9926  inrresf  9928  djuun  9938  cardlim  9984  infxpenlem  10025  alephfp  10120  cfsmolem  10282  alephsing  10288  hsmexlem4  10441  axdc3lem2  10463  numth3  10482  iunfo  10551  konigthlem  10580  iunctb  10586  canthwelem  10662  canthwe  10663  r1limwun  10748  inar1  10787  inatsk  10790  gruina  10830  grur1  10832  tskmval  10851  tskmcl  10853  pinq  10939  dmrecnq  10980  addclsr  11095  mulclsr  11096  axaddf  11157  axmulf  11158  peano2nn  12250  uztrn2  12869  eluz2nn  12896  peano2uzs  12916  uzsupss  12954  uzsup  13878  uzrdgfni  13974  uzrdgsuci  13976  fsuppmapnn0fiub  14007  seqf  14039  ser0  14070  bcm1k  14331  bcp1nk  14333  bcpasc  14337  hashprdifel  14414  fz1isolem  14477  pr2pwpr  14495  tpf  14515  ccats1val2  14643  rexuzre  15369  limsupgre  15495  climconst  15557  rlimclim1  15559  climrlim2  15561  clim2ser  15669  clim2ser2  15670  iserex  15671  isermulc2  15672  iserle  15674  isercolllem3  15681  isercoll2  15683  climsup  15684  iseraltlem2  15697  iseraltlem3  15698  zsum  15732  isumclim3  15773  isumadd  15781  fsump1i  15783  iserabs  15829  cvgcmp  15830  cvgcmpub  15831  cvgcmpce  15832  abscvgcvg  15833  isumshft  15853  isumsplit  15854  isum1p  15855  isumrpcl  15857  isumsup2  15860  climcndslem1  15863  cvgrat  15897  clim2prod  15902  clim2div  15903  prodf1  15905  ntrivcvgn0  15912  ntrivcvgtail  15914  fprodntriv  15956  fprodabs  15988  fprodeq0  15989  iprodclim3  16014  iprodmul  16017  ef0lem  16092  fprodefsum  16109  rpnnen2lem3  16232  dvdsflip  16334  fzo0dvdseq  16340  bitsinv1  16459  smupval  16505  smueqlem  16507  seq1st  16588  algr0  16589  prmind2  16702  crth  16795  eulerthlem2  16799  prmdiv  16802  pockthlem  16923  pockthg  16924  unbenlem  16926  prmunb  16932  prmgaplem7  17075  strfv2d  17218  imasvscaval  17550  oppccatid  17729  oppccatf  17738  epii  17754  fthepi  17941  funcestrcsetclem3  18152  funcsetcestrclem3  18166  yon12  18275  yon2  18276  yonedalem4c  18287  yonedalem22  18288  yonedalem3b  18289  yonedainv  18291  acsmapd  18562  mgm2nsgrplem1  18894  mgm2nsgrplem2  18895  mgm2nsgrplem3  18896  sgrp2nmndlem1  18899  sgrp2rid2  18902  ghmqusker  19268  cntrsubgnsg  19324  symgpssefmnd  19375  pmtrrn  19436  gexcl3  19566  efgi  19698  efgi2  19704  efgs1b  19715  efgredlemg  19721  efgredlemd  19723  frgpnabllem1  19852  cycsubgcyg  19880  gsumzaddlem  19900  dprdwd  19992  dprd2da  20023  rhmopp  20467  lsppratlem3  21108  lsppratlem4  21109  lbsextlem2  21118  lidl0ALT  21187  lidl1ALT  21190  2idl0  21219  2idl1  21220  domnchr  21491  znf1o  21510  mplsubrglem  21962  mpfconst  22057  mpfproj  22058  mpfind  22063  mhpmulcl  22085  pf1const  22282  pf1id  22283  mpfpf1  22287  pf1mpf  22288  madetsumid  22397  slesolex  22618  pmatcoe1fsupp  22637  mat2pmatbas0  22663  pmatcollpw  22717  pm2mpf1  22735  isclo  23023  indiscld  23027  restntr  23118  ordtbaslem  23124  ordtbas2  23127  lmconst  23197  lmss  23234  conncompid  23367  2ndcomap  23394  locfincmp  23462  comppfsc  23468  xkouni  23535  txcls  23540  ptclsg  23551  uptx  23561  txindis  23570  tx1stc  23586  cnmpt1res  23612  tgqtop  23648  uffix  23857  cnpflf2  23936  ptcmplem2  23989  ptcmplem4  23991  tgpconncomp  24049  tsmsfbas  24064  fmucnd  24228  prdsxmetlem  24305  imasdsf1olem  24310  prdsbl  24428  blcvx  24735  xrsmopn  24750  xrge0tsms  24772  metdcn2  24777  expcncf  24869  cnmpopc  24871  icchmeo  24887  icchmeoOLD  24888  iccpnfhmeo  24892  cnheibor  24903  evth  24907  evth2  24908  lebnumlem2  24910  lebnumii  24914  reparphti  24945  reparphtiOLD  24946  cfilfcls  25224  minveclem2  25376  minveclem3  25379  minveclem4  25382  ovoliunlem1  25453  ovolicc1  25467  iundisj  25499  volsup  25507  uniioombllem3  25536  vitalilem2  25560  vitalilem3  25561  mbfsup  25615  mbfinf  25616  mbflimsup  25617  itg2monolem1  25701  limcflflem  25831  limccnp  25842  limccnp2  25843  dvidlem  25866  dvn2bss  25882  cpnres  25889  dvcobr  25899  dvcobrOLD  25900  dvrec  25909  c1liplem1  25951  dvcnvrelem2  25973  dvfsumrlimf  25981  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsumrlim  25988  dvfsum2  25991  coeeulem  26179  coeid3  26195  plycn  26216  plycnOLD  26217  dvntaylp  26329  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulm2  26344  ulmshftlem  26348  ulmshft  26349  ulm0  26350  ulmcn  26358  ulmdvlem3  26361  ulmdv  26362  mtest  26363  mtestbdd  26364  dvradcnv  26380  psercn2  26382  psercn2OLD  26383  psercn  26386  pserdv  26389  abelth  26401  efif1olem2  26502  efif1olem4  26504  efifo  26506  eff1olem  26507  logcn  26606  dvloglem  26607  cxpcn3  26708  resqrtcn  26709  sqrtcn  26710  logbleb  26743  logblt  26744  asinneg  26846  atanlogsub  26876  atanbnd  26886  ressatans  26894  leibpilem2  26901  xrlimcnp  26928  efrlim  26929  efrlimOLD  26930  scvxcvx  26946  ppiub  27165  chtub  27173  logexprlim  27186  lgseisenlem1  27336  rplogsumlem1  27445  rplogsumlem2  27446  dchrisumlem2  27451  dchrisum0flb  27471  logdivbnd  27517  pntlem3  27570  dfnns2  28279  tgcgr4  28456  ltgov  28522  f1otrg  28796  eengtrkg  28911  iedgedg  28975  ushgredgedgloop  29156  subgruhgredgd  29209  uvtxupgrres  29333  umgr2v2evd2  29453  edginwlk  29561  wlk1walk  29565  crctcshwlkn0lem6  29743  wlkiswwlks1  29795  minvecolem1  30801  minvecolem2  30802  minvecolem4  30807  htthlem  30844  5oalem2  31582  3oalem2  31590  iundisjf  32516  fmptco1f1o  32557  xppreima  32569  xppreima2  32575  dfcnv2  32600  ccatws1f1o  32873  chnub  32938  chnccats1  32941  gsumhashmul  33001  xrge0tsmsd  33002  gsumwrd2dccatlem  33006  odpmco  33043  pmtrcnelor  33048  fzo0pmtrlast  33049  wrdpmtrlast  33050  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1stfv1  33058  fzto1st  33060  fzto1stinvn  33061  psgnfzto1st  33062  tocycf  33074  cycpmco2lem7  33089  cycpmco2  33090  cycpmrn  33100  cyc3evpm  33107  cyc3genpmlem  33108  cycpmgcl  33110  cyc3conja  33114  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspnsubrunlem1  33188  nsgmgc  33373  nsgqusf1olem1  33374  nsgqusf1olem2  33375  rhmpreimaprmidl  33412  ssdifidllem  33417  ssdifidl  33418  ssmxidllem  33434  drngmxidlr  33439  opprqus1r  33453  qsdrngilem  33455  qsdrngi  33456  rsprprmprmidlb  33484  rprmirredb  33493  1arithufdlem1  33505  1arithufdlem2  33506  1arithufdlem3  33507  1arithufdlem4  33508  fply1  33517  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ply1degltdimlem  33608  ply1degltdim  33609  algextdeglem4  33700  algextdeglem6  33702  algextdeglem7  33703  algextdeglem8  33704  nn0constr  33741  smatlem  33774  smatcl  33779  zartopn  33852  zarmxt1  33857  tpr2rico  33889  xrmulc1cn  33907  xrge0mulc1cn  33918  esumpfinvallem  34051  ldgenpisyslem1  34140  dynkin  34144  brfae  34225  sxbrsigalem3  34250  dya2icoseg2  34256  omsmeas  34301  sibfof  34318  sseqmw  34369  sseqf  34370  sseqp1  34373  fiblem  34376  fibp1  34379  probfinmeasbALTV  34407  repr0  34589  reprpmtf1o  34604  hgt750lemg  34632  bnj1379  34807  srcmpltd  35057  subfacp1lem5  35152  subfacp1lem6  35153  cvxpconn  35210  cvxsconn  35211  cvmliftlem6  35258  cvmliftlem8  35260  cvmliftlem10  35262  cvmlift2lem6  35276  cvmlift2lem11  35281  cvmlift2lem12  35282  2goelgoanfmla1  35392  prv1n  35399  msubff  35498  msubco  35499  elmsta  35516  msubff1  35524  mvhf  35526  msubvrs  35528  iprodefisumlem  35703  filnetlem3  36344  knoppcnlem10  36466  knoppcnlem11  36467  icoreunrn  37323  icoreelrn  37325  ralssiun  37371  poimirlem3  37593  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem30  37620  dvasin  37674  cover2  37685  upixp  37699  sdclem1  37713  fdc  37715  caushft  37731  ismtyres  37778  rrncmslem  37802  isfld2  37975  osumcllem10N  39930  pexmidlem7N  39941  dihglblem2N  41259  lcfrvalsnN  41506  lcfrlem5  41511  lcfrlem6  41512  lcfrlem27  41534  lcfrlem37  41544  aks6d1c1p4  42070  aks6d1c1p7  42072  aks6d1c1p8  42074  evl1gprodd  42076  aks6d1c2lem4  42086  aks6d1c5lem3  42096  aks6d1c6lem2  42130  prjspvs  42580  0prjspnrel  42597  monotuz  42912  expdiophlem1  42992  kelac2  43036  naddwordnexlem4  43372  grurankcld  44205  dvgrat  44284  nzss  44289  uzmptshftfval  44318  binomcxplemnotnn0  44328  orbitinit  44929  orbitcl  44930  permaxinf2lem  44985  refsumcn  45002  rfcnpre2  45003  rfcnpre3  45005  rfcnpre4  45006  disjf1o  45163  unirnmap  45180  unirnmapsn  45186  ssmapsn  45188  mptssid  45213  allbutfi  45368  eluzd  45384  uzidd2  45391  ressiocsup  45531  ressioosup  45532  ressiooinf  45534  fsumsermpt  45556  climexp  45582  climinf  45583  climsuse  45585  sumnnodd  45607  limsupresico  45677  limsupubuzlem  45689  limsupresxr  45743  liminfresxr  45744  liminfresico  45748  limsup10exlem  45749  cnrefiisplem  45806  cncfiooicclem1  45870  dvsinax  45890  itgsinexplem1  45931  fvvolioof  45966  fvvolicof  45968  stoweidlem14  45991  stoweidlem16  45993  stoweidlem31  46008  stoweidlem34  46011  stoweidlem36  46013  stoweidlem43  46020  stoweidlem46  46023  stoweidlem47  46024  stoweidlem52  46029  stoweidlem55  46032  stoweidlem57  46034  dirkercncf  46084  fourierdlem20  46104  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem51  46134  fourierdlem54  46137  fourierdlem62  46145  fourierdlem71  46154  fourierdlem80  46163  fourierdlem114  46197  fouriersw  46208  ioorrnopnlem  46281  ioorrnopnxrlem  46283  salexct3  46319  salgencntex  46320  salgensscntex  46321  subsalsal  46336  sge0fodjrnlem  46393  sge0isum  46404  sge0seq  46423  sge0reuz  46424  sge0reuzb  46425  meadjiunlem  46442  meaiininclem  46463  carageniuncllem1  46498  caratheodorylem1  46503  hoiprodp1  46565  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  voncmpl  46598  hoiqssbl  46602  smflimlem2  46749  smfsuplem1  46788  smfsuplem3  46790  fsupdm  46819  finfdm  46823  cfsetsnfsetf  47035  fcores  47044  afvres  47149  afv2res  47216  fundcmpsurinjimaid  47373  iccpartigtl  47385  sprsymrelf  47457  prproropf1olem2  47466  uhgrimedgi  47851  isuspgrim0lem  47854  isuspgrimlem  47856  ushggricedg  47888  grimedg  47896  usgrgrtrirex  47910  isubgr3stgrlem7  47932  uspgrlimlem4  47951  gpgiedgdmellem  47998  gpg3kgrtriex  48039  funcringcsetcALTV2lem3  48215  funcringcsetclem3ALTV  48238  lindslinindsimp2lem5  48386  rrxsphere  48676  line2  48680  iooii  48840  icccldii  48841  iscnrm3rlem3  48864  oppcup  49088  zeroo2  49099  2arwcat  49425  incat  49426  onsetreclem3  49519  amgmwlem  49614