Theorem eleqtrrdi 2839

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 2738	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2838	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 2701

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

This theorem is referenced by:  3eltr4g  2845  brelrng  5894  elabrex  7198  elabrexg  7199  fliftel1  7267  ovidig  7511  unielxp  7985  tfrlem11  8333  rdglim  8371  seqomlem4  8398  2oconcl  8444  ecopqsi  8721  erov  8764  eroprf  8765  sbthlem2  9029  dffi3  9358  ixpiunwdom  9519  cantnfcl  9596  r1lim  9701  rankwflemb  9722  pwwf  9736  unwf  9739  rankwflem  9744  uniwf  9748  rankpwi  9752  rankr1g  9761  r1pw  9774  r1rankid  9788  rankuni  9792  djulcl  9839  djurcl  9840  inlresf  9843  inrresf  9845  djuun  9855  cardlim  9901  infxpenlem  9942  alephfp  10037  cfsmolem  10199  alephsing  10205  hsmexlem4  10358  axdc3lem2  10380  numth3  10399  iunfo  10468  konigthlem  10497  iunctb  10503  canthwelem  10579  canthwe  10580  r1limwun  10665  inar1  10704  inatsk  10707  gruina  10747  grur1  10749  tskmval  10768  tskmcl  10770  pinq  10856  dmrecnq  10897  addclsr  11012  mulclsr  11013  axaddf  11074  axmulf  11075  peano2nn  12174  uztrn2  12788  eluz2nn  12823  peano2uzs  12837  uzsupss  12875  uzsup  13801  uzrdgfni  13899  uzrdgsuci  13901  fsuppmapnn0fiub  13932  seqf  13964  ser0  13995  bcm1k  14256  bcp1nk  14258  bcpasc  14262  hashprdifel  14339  fz1isolem  14402  pr2pwpr  14420  tpf  14440  ccats1val2  14568  rexuzre  15295  limsupgre  15423  climconst  15485  rlimclim1  15487  climrlim2  15489  clim2ser  15597  clim2ser2  15598  iserex  15599  isermulc2  15600  iserle  15602  isercolllem3  15609  isercoll2  15611  climsup  15612  iseraltlem2  15625  iseraltlem3  15626  zsum  15660  isumclim3  15701  isumadd  15709  fsump1i  15711  iserabs  15757  cvgcmp  15758  cvgcmpub  15759  cvgcmpce  15760  abscvgcvg  15761  isumshft  15781  isumsplit  15782  isum1p  15783  isumrpcl  15785  isumsup2  15788  climcndslem1  15791  cvgrat  15825  clim2prod  15830  clim2div  15831  prodf1  15833  ntrivcvgn0  15840  ntrivcvgtail  15842  fprodntriv  15884  fprodabs  15916  fprodeq0  15917  iprodclim3  15942  iprodmul  15945  ef0lem  16020  fprodefsum  16037  rpnnen2lem3  16160  dvdsflip  16263  fzo0dvdseq  16269  bitsinv1  16388  smupval  16434  smueqlem  16436  seq1st  16517  algr0  16518  prmind2  16631  crth  16724  eulerthlem2  16728  prmdiv  16731  pockthlem  16852  pockthg  16853  unbenlem  16855  prmunb  16861  prmgaplem7  17004  strfv2d  17147  imasvscaval  17477  oppccatid  17660  oppccatf  17669  epii  17685  fthepi  17872  funcestrcsetclem3  18083  funcsetcestrclem3  18097  yon12  18206  yon2  18207  yonedalem4c  18218  yonedalem22  18219  yonedalem3b  18220  yonedainv  18222  acsmapd  18495  mgm2nsgrplem1  18827  mgm2nsgrplem2  18828  mgm2nsgrplem3  18829  sgrp2nmndlem1  18832  sgrp2rid2  18835  ghmqusker  19201  cntrsubgnsg  19257  symgpssefmnd  19310  pmtrrn  19371  gexcl3  19501  efgi  19633  efgi2  19639  efgs1b  19650  efgredlemg  19656  efgredlemd  19658  frgpnabllem1  19787  cycsubgcyg  19815  gsumzaddlem  19835  dprdwd  19927  dprd2da  19958  rhmopp  20429  lsppratlem3  21091  lsppratlem4  21092  lbsextlem2  21101  lidl0ALT  21170  lidl1ALT  21173  2idl0  21202  2idl1  21203  domnchr  21474  znf1o  21493  mplsubrglem  21946  mpfconst  22041  mpfproj  22042  mpfind  22047  mhpmulcl  22069  pf1const  22266  pf1id  22267  mpfpf1  22271  pf1mpf  22272  madetsumid  22381  slesolex  22602  pmatcoe1fsupp  22621  mat2pmatbas0  22647  pmatcollpw  22701  pm2mpf1  22719  isclo  23007  indiscld  23011  restntr  23102  ordtbaslem  23108  ordtbas2  23111  lmconst  23181  lmss  23218  conncompid  23351  2ndcomap  23378  locfincmp  23446  comppfsc  23452  xkouni  23519  txcls  23524  ptclsg  23535  uptx  23545  txindis  23554  tx1stc  23570  cnmpt1res  23596  tgqtop  23632  uffix  23841  cnpflf2  23920  ptcmplem2  23973  ptcmplem4  23975  tgpconncomp  24033  tsmsfbas  24048  fmucnd  24212  prdsxmetlem  24289  imasdsf1olem  24294  prdsbl  24412  blcvx  24719  xrsmopn  24734  xrge0tsms  24756  metdcn2  24761  expcncf  24853  cnmpopc  24855  icchmeo  24871  icchmeoOLD  24872  iccpnfhmeo  24876  cnheibor  24887  evth  24891  evth2  24892  lebnumlem2  24894  lebnumii  24898  reparphti  24929  reparphtiOLD  24930  cfilfcls  25207  minveclem2  25359  minveclem3  25362  minveclem4  25365  ovoliunlem1  25436  ovolicc1  25450  iundisj  25482  volsup  25490  uniioombllem3  25519  vitalilem2  25543  vitalilem3  25544  mbfsup  25598  mbfinf  25599  mbflimsup  25600  itg2monolem1  25684  limcflflem  25814  limccnp  25825  limccnp2  25826  dvidlem  25849  dvn2bss  25865  cpnres  25872  dvcobr  25882  dvcobrOLD  25883  dvrec  25892  c1liplem1  25934  dvcnvrelem2  25956  dvfsumrlimf  25964  dvfsumlem1  25965  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  dvfsumlem4  25969  dvfsumrlim  25971  dvfsum2  25974  coeeulem  26162  coeid3  26178  plycn  26199  plycnOLD  26200  dvntaylp  26312  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulm2  26327  ulmshftlem  26331  ulmshft  26332  ulm0  26333  ulmcn  26341  ulmdvlem3  26344  ulmdv  26345  mtest  26346  mtestbdd  26347  dvradcnv  26363  psercn2  26365  psercn2OLD  26366  psercn  26369  pserdv  26372  abelth  26384  efif1olem2  26485  efif1olem4  26487  efifo  26489  eff1olem  26490  logcn  26589  dvloglem  26590  cxpcn3  26691  resqrtcn  26692  sqrtcn  26693  logbleb  26726  logblt  26727  asinneg  26829  atanlogsub  26859  atanbnd  26869  ressatans  26877  leibpilem2  26884  xrlimcnp  26911  efrlim  26912  efrlimOLD  26913  scvxcvx  26929  ppiub  27148  chtub  27156  logexprlim  27169  lgseisenlem1  27319  rplogsumlem1  27428  rplogsumlem2  27429  dchrisumlem2  27434  dchrisum0flb  27454  logdivbnd  27500  pntlem3  27553  dfnns2  28301  tgcgr4  28511  ltgov  28577  f1otrg  28851  eengtrkg  28966  iedgedg  29030  ushgredgedgloop  29211  subgruhgredgd  29264  uvtxupgrres  29388  umgr2v2evd2  29508  edginwlk  29615  wlk1walk  29619  crctcshwlkn0lem6  29795  wlkiswwlks1  29847  minvecolem1  30853  minvecolem2  30854  minvecolem4  30859  htthlem  30896  5oalem2  31634  3oalem2  31642  iundisjf  32568  fmptco1f1o  32607  xppreima  32619  xppreima2  32625  dfcnv2  32650  ccatws1f1o  32923  chnub  32984  chnccats1  32987  gsumhashmul  33044  xrge0tsmsd  33045  gsumwrd2dccatlem  33049  odpmco  33058  pmtrcnelor  33063  fzo0pmtrlast  33064  wrdpmtrlast  33065  pmtrto1cl  33071  psgnfzto1stlem  33072  fzto1stfv1  33073  fzto1st  33075  fzto1stinvn  33076  psgnfzto1st  33077  tocycf  33089  cycpmco2lem7  33104  cycpmco2  33105  cycpmrn  33115  cyc3evpm  33122  cyc3genpmlem  33123  cycpmgcl  33125  cyc3conja  33129  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnlem4  33212  elrgspnsubrunlem1  33214  nsgmgc  33376  nsgqusf1olem1  33377  nsgqusf1olem2  33378  rhmpreimaprmidl  33415  ssdifidllem  33420  ssdifidl  33421  ssmxidllem  33437  drngmxidlr  33442  opprqus1r  33456  qsdrngilem  33458  qsdrngi  33459  rsprprmprmidlb  33487  rprmirredb  33496  1arithufdlem1  33508  1arithufdlem2  33509  1arithufdlem3  33510  1arithufdlem4  33511  fply1  33520  ply1degltel  33553  ply1degleel  33554  ply1degltlss  33555  ply1degltdimlem  33611  ply1degltdim  33612  algextdeglem4  33703  algextdeglem6  33705  algextdeglem7  33706  algextdeglem8  33707  nn0constr  33744  smatlem  33780  smatcl  33785  zartopn  33858  zarmxt1  33863  tpr2rico  33895  xrmulc1cn  33913  xrge0mulc1cn  33924  esumpfinvallem  34057  ldgenpisyslem1  34146  dynkin  34150  brfae  34231  sxbrsigalem3  34256  dya2icoseg2  34262  omsmeas  34307  sibfof  34324  sseqmw  34375  sseqf  34376  sseqp1  34379  fiblem  34382  fibp1  34385  probfinmeasbALTV  34413  repr0  34595  reprpmtf1o  34610  hgt750lemg  34638  bnj1379  34813  srcmpltd  35063  subfacp1lem5  35164  subfacp1lem6  35165  cvxpconn  35222  cvxsconn  35223  cvmliftlem6  35270  cvmliftlem8  35272  cvmliftlem10  35274  cvmlift2lem6  35288  cvmlift2lem11  35293  cvmlift2lem12  35294  2goelgoanfmla1  35404  prv1n  35411  msubff  35510  msubco  35511  elmsta  35528  msubff1  35536  mvhf  35538  msubvrs  35540  iprodefisumlem  35720  filnetlem3  36361  knoppcnlem10  36483  knoppcnlem11  36484  icoreunrn  37340  icoreelrn  37342  ralssiun  37388  poimirlem3  37610  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem30  37637  dvasin  37691  cover2  37702  upixp  37716  sdclem1  37730  fdc  37732  caushft  37748  ismtyres  37795  rrncmslem  37819  isfld2  37992  osumcllem10N  39952  pexmidlem7N  39963  dihglblem2N  41281  lcfrvalsnN  41528  lcfrlem5  41533  lcfrlem6  41534  lcfrlem27  41556  lcfrlem37  41566  aks6d1c1p4  42092  aks6d1c1p7  42094  aks6d1c1p8  42096  evl1gprodd  42098  aks6d1c2lem4  42108  aks6d1c5lem3  42118  aks6d1c6lem2  42152  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  47052  fcores  47061  afvres  47166  afv2res  47233  fundcmpsurinjimaid  47405  iccpartigtl  47417  sprsymrelf  47489  prproropf1olem2  47498  uhgrimedgi  47883  isuspgrim0lem  47886  isuspgrimlem  47888  ushggricedg  47920  grimedg  47928  usgrgrtrirex  47942  isubgr3stgrlem7  47964  uspgrlimlem4  47983  gpgiedgdmellem  48030  gpg3kgrtriex  48073  funcringcsetcALTV2lem3  48273  funcringcsetclem3ALTV  48296  lindslinindsimp2lem5  48444  rrxsphere  48730  line2  48734  iooii  48899  icccldii  48900  iscnrm3rlem3  48923  eloppf2  49116  oppcup  49189  natoppf  49211  zeroo2  49216  oppfdiag1  49396  oppfdiag  49398  2arwcat  49582  incat  49583  lmddu  49649  onsetreclem3  49689  amgmwlem  49784