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  5883  elabrex  7178  elabrexg  7179  fliftel1  7247  ovidig  7491  unielxp  7962  tfrlem11  8310  rdglim  8348  seqomlem4  8375  2oconcl  8421  ecopqsi  8698  erov  8741  eroprf  8742  sbthlem2  9005  dffi3  9321  ixpiunwdom  9482  cantnfcl  9563  r1lim  9668  rankwflemb  9689  pwwf  9703  unwf  9706  rankwflem  9711  uniwf  9715  rankpwi  9719  rankr1g  9728  r1pw  9741  r1rankid  9755  rankuni  9759  djulcl  9806  djurcl  9807  inlresf  9810  inrresf  9812  djuun  9822  cardlim  9868  infxpenlem  9907  alephfp  10002  cfsmolem  10164  alephsing  10170  hsmexlem4  10323  axdc3lem2  10345  numth3  10364  iunfo  10433  konigthlem  10462  iunctb  10468  canthwelem  10544  canthwe  10545  r1limwun  10630  inar1  10669  inatsk  10672  gruina  10712  grur1  10714  tskmval  10733  tskmcl  10735  pinq  10821  dmrecnq  10862  addclsr  10977  mulclsr  10978  axaddf  11039  axmulf  11040  peano2nn  12140  uztrn2  12754  eluz2nn  12789  peano2uzs  12803  uzsupss  12841  uzsup  13767  uzrdgfni  13865  uzrdgsuci  13867  fsuppmapnn0fiub  13898  seqf  13930  ser0  13961  bcm1k  14222  bcp1nk  14224  bcpasc  14228  hashprdifel  14305  fz1isolem  14368  pr2pwpr  14386  tpf  14406  ccats1val2  14534  rexuzre  15260  limsupgre  15388  climconst  15450  rlimclim1  15452  climrlim2  15454  clim2ser  15562  clim2ser2  15563  iserex  15564  isermulc2  15565  iserle  15567  isercolllem3  15574  isercoll2  15576  climsup  15577  iseraltlem2  15590  iseraltlem3  15591  zsum  15625  isumclim3  15666  isumadd  15674  fsump1i  15676  iserabs  15722  cvgcmp  15723  cvgcmpub  15724  cvgcmpce  15725  abscvgcvg  15726  isumshft  15746  isumsplit  15747  isum1p  15748  isumrpcl  15750  isumsup2  15753  climcndslem1  15756  cvgrat  15790  clim2prod  15795  clim2div  15796  prodf1  15798  ntrivcvgn0  15805  ntrivcvgtail  15807  fprodntriv  15849  fprodabs  15881  fprodeq0  15882  iprodclim3  15907  iprodmul  15910  ef0lem  15985  fprodefsum  16002  rpnnen2lem3  16125  dvdsflip  16228  fzo0dvdseq  16234  bitsinv1  16353  smupval  16399  smueqlem  16401  seq1st  16482  algr0  16483  prmind2  16596  crth  16689  eulerthlem2  16693  prmdiv  16696  pockthlem  16817  pockthg  16818  unbenlem  16820  prmunb  16826  prmgaplem7  16969  strfv2d  17112  imasvscaval  17442  oppccatid  17625  oppccatf  17634  epii  17650  fthepi  17837  funcestrcsetclem3  18048  funcsetcestrclem3  18062  yon12  18171  yon2  18172  yonedalem4c  18183  yonedalem22  18184  yonedalem3b  18185  yonedainv  18187  acsmapd  18460  mgm2nsgrplem1  18792  mgm2nsgrplem2  18793  mgm2nsgrplem3  18794  sgrp2nmndlem1  18797  sgrp2rid2  18800  ghmqusker  19166  cntrsubgnsg  19222  symgpssefmnd  19275  pmtrrn  19336  gexcl3  19466  efgi  19598  efgi2  19604  efgs1b  19615  efgredlemg  19621  efgredlemd  19623  frgpnabllem1  19752  cycsubgcyg  19780  gsumzaddlem  19800  dprdwd  19892  dprd2da  19923  rhmopp  20394  lsppratlem3  21056  lsppratlem4  21057  lbsextlem2  21066  lidl0ALT  21135  lidl1ALT  21138  2idl0  21167  2idl1  21168  domnchr  21439  znf1o  21458  mplsubrglem  21911  mpfconst  22006  mpfproj  22007  mpfind  22012  mhpmulcl  22034  pf1const  22231  pf1id  22232  mpfpf1  22236  pf1mpf  22237  madetsumid  22346  slesolex  22567  pmatcoe1fsupp  22586  mat2pmatbas0  22612  pmatcollpw  22666  pm2mpf1  22684  isclo  22972  indiscld  22976  restntr  23067  ordtbaslem  23073  ordtbas2  23076  lmconst  23146  lmss  23183  conncompid  23316  2ndcomap  23343  locfincmp  23411  comppfsc  23417  xkouni  23484  txcls  23489  ptclsg  23500  uptx  23510  txindis  23519  tx1stc  23535  cnmpt1res  23561  tgqtop  23597  uffix  23806  cnpflf2  23885  ptcmplem2  23938  ptcmplem4  23940  tgpconncomp  23998  tsmsfbas  24013  fmucnd  24177  prdsxmetlem  24254  imasdsf1olem  24259  prdsbl  24377  blcvx  24684  xrsmopn  24699  xrge0tsms  24721  metdcn2  24726  expcncf  24818  cnmpopc  24820  icchmeo  24836  icchmeoOLD  24837  iccpnfhmeo  24841  cnheibor  24852  evth  24856  evth2  24857  lebnumlem2  24859  lebnumii  24863  reparphti  24894  reparphtiOLD  24895  cfilfcls  25172  minveclem2  25324  minveclem3  25327  minveclem4  25330  ovoliunlem1  25401  ovolicc1  25415  iundisj  25447  volsup  25455  uniioombllem3  25484  vitalilem2  25508  vitalilem3  25509  mbfsup  25563  mbfinf  25564  mbflimsup  25565  itg2monolem1  25649  limcflflem  25779  limccnp  25790  limccnp2  25791  dvidlem  25814  dvn2bss  25830  cpnres  25837  dvcobr  25847  dvcobrOLD  25848  dvrec  25857  c1liplem1  25899  dvcnvrelem2  25921  dvfsumrlimf  25929  dvfsumlem1  25930  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem3  25933  dvfsumlem4  25934  dvfsumrlim  25936  dvfsum2  25939  coeeulem  26127  coeid3  26143  plycn  26164  plycnOLD  26165  dvntaylp  26277  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulm2  26292  ulmshftlem  26296  ulmshft  26297  ulm0  26298  ulmcn  26306  ulmdvlem3  26309  ulmdv  26310  mtest  26311  mtestbdd  26312  dvradcnv  26328  psercn2  26330  psercn2OLD  26331  psercn  26334  pserdv  26337  abelth  26349  efif1olem2  26450  efif1olem4  26452  efifo  26454  eff1olem  26455  logcn  26554  dvloglem  26555  cxpcn3  26656  resqrtcn  26657  sqrtcn  26658  logbleb  26691  logblt  26692  asinneg  26794  atanlogsub  26824  atanbnd  26834  ressatans  26842  leibpilem2  26849  xrlimcnp  26876  efrlim  26877  efrlimOLD  26878  scvxcvx  26894  ppiub  27113  chtub  27121  logexprlim  27134  lgseisenlem1  27284  rplogsumlem1  27393  rplogsumlem2  27394  dchrisumlem2  27399  dchrisum0flb  27419  logdivbnd  27465  pntlem3  27518  dfnns2  28266  tgcgr4  28476  ltgov  28542  f1otrg  28816  eengtrkg  28931  iedgedg  28995  ushgredgedgloop  29176  subgruhgredgd  29229  uvtxupgrres  29353  umgr2v2evd2  29473  edginwlk  29580  wlk1walk  29584  crctcshwlkn0lem6  29760  wlkiswwlks1  29812  minvecolem1  30818  minvecolem2  30819  minvecolem4  30824  htthlem  30861  5oalem2  31599  3oalem2  31607  iundisjf  32533  fmptco1f1o  32576  xppreima  32588  xppreima2  32594  dfcnv2  32619  ccatws1f1o  32893  chnub  32954  chnccats1  32957  gsumhashmul  33014  xrge0tsmsd  33015  gsumwrd2dccatlem  33019  odpmco  33028  pmtrcnelor  33033  fzo0pmtrlast  33034  wrdpmtrlast  33035  pmtrto1cl  33041  psgnfzto1stlem  33042  fzto1stfv1  33043  fzto1st  33045  fzto1stinvn  33046  psgnfzto1st  33047  tocycf  33059  cycpmco2lem7  33074  cycpmco2  33075  cycpmrn  33085  cyc3evpm  33092  cyc3genpmlem  33093  cycpmgcl  33095  cyc3conja  33099  elrgspnlem1  33182  elrgspnlem2  33183  elrgspnlem3  33184  elrgspnlem4  33185  elrgspnsubrunlem1  33187  nsgmgc  33349  nsgqusf1olem1  33350  nsgqusf1olem2  33351  rhmpreimaprmidl  33388  ssdifidllem  33393  ssdifidl  33394  ssmxidllem  33410  drngmxidlr  33415  opprqus1r  33429  qsdrngilem  33431  qsdrngi  33432  rsprprmprmidlb  33460  rprmirredb  33469  1arithufdlem1  33481  1arithufdlem2  33482  1arithufdlem3  33483  1arithufdlem4  33484  fply1  33493  ply1degltel  33527  ply1degleel  33528  ply1degltlss  33529  ply1degltdimlem  33589  ply1degltdim  33590  algextdeglem4  33687  algextdeglem6  33689  algextdeglem7  33690  algextdeglem8  33691  nn0constr  33728  smatlem  33764  smatcl  33769  zartopn  33842  zarmxt1  33847  tpr2rico  33879  xrmulc1cn  33897  xrge0mulc1cn  33908  esumpfinvallem  34041  ldgenpisyslem1  34130  dynkin  34134  brfae  34215  sxbrsigalem3  34240  dya2icoseg2  34246  omsmeas  34291  sibfof  34308  sseqmw  34359  sseqf  34360  sseqp1  34363  fiblem  34366  fibp1  34369  probfinmeasbALTV  34397  repr0  34579  reprpmtf1o  34594  hgt750lemg  34622  bnj1379  34797  srcmpltd  35047  fineqvnttrclselem3  35076  subfacp1lem5  35161  subfacp1lem6  35162  cvxpconn  35219  cvxsconn  35220  cvmliftlem6  35267  cvmliftlem8  35269  cvmliftlem10  35271  cvmlift2lem6  35285  cvmlift2lem11  35290  cvmlift2lem12  35291  2goelgoanfmla1  35401  prv1n  35408  msubff  35507  msubco  35508  elmsta  35525  msubff1  35533  mvhf  35535  msubvrs  35537  iprodefisumlem  35717  filnetlem3  36358  knoppcnlem10  36480  knoppcnlem11  36481  icoreunrn  37337  icoreelrn  37339  ralssiun  37385  poimirlem3  37607  poimirlem16  37620  poimirlem17  37621  poimirlem19  37623  poimirlem30  37634  dvasin  37688  cover2  37699  upixp  37713  sdclem1  37727  fdc  37729  caushft  37745  ismtyres  37792  rrncmslem  37816  isfld2  37989  osumcllem10N  39948  pexmidlem7N  39959  dihglblem2N  41277  lcfrvalsnN  41524  lcfrlem5  41529  lcfrlem6  41530  lcfrlem27  41552  lcfrlem37  41562  aks6d1c1p4  42088  aks6d1c1p7  42090  aks6d1c1p8  42092  evl1gprodd  42094  aks6d1c2lem4  42104  aks6d1c5lem3  42114  aks6d1c6lem2  42148  prjspvs  42587  0prjspnrel  42604  monotuz  42918  expdiophlem1  42998  kelac2  43042  naddwordnexlem4  43378  grurankcld  44210  dvgrat  44289  nzss  44294  uzmptshftfval  44323  binomcxplemnotnn0  44333  orbitinit  44934  orbitcl  44935  permaxinf2lem  44990  refsumcn  45012  rfcnpre2  45013  rfcnpre3  45015  rfcnpre4  45016  disjf1o  45173  unirnmap  45190  unirnmapsn  45196  ssmapsn  45198  mptssid  45223  allbutfi  45376  eluzd  45392  uzidd2  45399  ressiocsup  45539  ressioosup  45540  ressiooinf  45542  fsumsermpt  45564  climexp  45590  climinf  45591  climsuse  45593  sumnnodd  45615  limsupresico  45685  limsupubuzlem  45697  limsupresxr  45751  liminfresxr  45752  liminfresico  45756  limsup10exlem  45757  cnrefiisplem  45814  cncfiooicclem1  45878  dvsinax  45898  itgsinexplem1  45939  fvvolioof  45974  fvvolicof  45976  stoweidlem14  45999  stoweidlem16  46001  stoweidlem31  46016  stoweidlem34  46019  stoweidlem36  46021  stoweidlem43  46028  stoweidlem46  46031  stoweidlem47  46032  stoweidlem52  46037  stoweidlem55  46040  stoweidlem57  46042  dirkercncf  46092  fourierdlem20  46112  fourierdlem42  46134  fourierdlem48  46139  fourierdlem49  46140  fourierdlem51  46142  fourierdlem54  46145  fourierdlem62  46153  fourierdlem71  46162  fourierdlem80  46171  fourierdlem114  46205  fouriersw  46216  ioorrnopnlem  46289  ioorrnopnxrlem  46291  salexct3  46327  salgencntex  46328  salgensscntex  46329  subsalsal  46344  sge0fodjrnlem  46401  sge0isum  46412  sge0seq  46431  sge0reuz  46432  sge0reuzb  46433  meadjiunlem  46450  meaiininclem  46471  carageniuncllem1  46506  caratheodorylem1  46511  hoiprodp1  46573  hoidmv1lelem1  46576  hoidmv1lelem2  46577  hoidmv1le  46579  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem3  46582  voncmpl  46606  hoiqssbl  46610  smflimlem2  46757  smfsuplem1  46796  smfsuplem3  46798  fsupdm  46827  finfdm  46831  cfsetsnfsetf  47046  fcores  47055  afvres  47160  afv2res  47227  fundcmpsurinjimaid  47399  iccpartigtl  47411  sprsymrelf  47483  prproropf1olem2  47492  uhgrimedgi  47878  isuspgrim0lem  47881  isuspgrimlem  47883  ushggricedg  47915  grimedg  47923  usgrgrtrirex  47938  isubgr3stgrlem7  47960  uspgrlimlem4  47979  grlimprclnbgr  47984  gpgiedgdmellem  48034  gpg3kgrtriex  48077  funcringcsetcALTV2lem3  48280  funcringcsetclem3ALTV  48303  lindslinindsimp2lem5  48451  rrxsphere  48737  line2  48741  iooii  48906  icccldii  48907  iscnrm3rlem3  48930  eloppf2  49123  oppcup  49196  natoppf  49218  zeroo2  49223  oppfdiag1  49403  oppfdiag  49405  2arwcat  49589  incat  49590  lmddu  49656  onsetreclem3  49696  amgmwlem  49791