Theorem eleqtrrdi 2852

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 2746	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2851	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 2708

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

This theorem is referenced by:  3eltr4g  2858  brelrng  5952  elabrex  7262  elabrexg  7263  fliftel1  7330  ovidig  7575  unielxp  8052  tfrlem11  8428  rdglim  8466  seqomlem4  8493  2oconcl  8541  ecopqsi  8814  erov  8854  eroprf  8855  sbthlem2  9124  dffi3  9471  ixpiunwdom  9630  cantnfcl  9707  r1lim  9812  rankwflemb  9833  pwwf  9847  unwf  9850  rankwflem  9855  uniwf  9859  rankpwi  9863  rankr1g  9872  r1pw  9885  r1rankid  9899  rankuni  9903  djulcl  9950  djurcl  9951  inlresf  9954  inrresf  9956  djuun  9966  cardlim  10012  infxpenlem  10053  alephfp  10148  cfsmolem  10310  alephsing  10316  hsmexlem4  10469  axdc3lem2  10491  numth3  10510  iunfo  10579  konigthlem  10608  iunctb  10614  canthwelem  10690  canthwe  10691  r1limwun  10776  inar1  10815  inatsk  10818  gruina  10858  grur1  10860  tskmval  10879  tskmcl  10881  pinq  10967  dmrecnq  11008  addclsr  11123  mulclsr  11124  axaddf  11185  axmulf  11186  peano2nn  12278  uztrn2  12897  eluz2nn  12924  peano2uzs  12944  uzsupss  12982  uzsup  13903  uzrdgfni  13999  uzrdgsuci  14001  fsuppmapnn0fiub  14032  seqf  14064  ser0  14095  bcm1k  14354  bcp1nk  14356  bcpasc  14360  hashprdifel  14437  fz1isolem  14500  pr2pwpr  14518  tpf  14538  ccats1val2  14665  rexuzre  15391  limsupgre  15517  climconst  15579  rlimclim1  15581  climrlim2  15583  clim2ser  15691  clim2ser2  15692  iserex  15693  isermulc2  15694  iserle  15696  isercolllem3  15703  isercoll2  15705  climsup  15706  iseraltlem2  15719  iseraltlem3  15720  zsum  15754  isumclim3  15795  isumadd  15803  fsump1i  15805  iserabs  15851  cvgcmp  15852  cvgcmpub  15853  cvgcmpce  15854  abscvgcvg  15855  isumshft  15875  isumsplit  15876  isum1p  15877  isumrpcl  15879  isumsup2  15882  climcndslem1  15885  cvgrat  15919  clim2prod  15924  clim2div  15925  prodf1  15927  ntrivcvgn0  15934  ntrivcvgtail  15936  fprodntriv  15978  fprodabs  16010  fprodeq0  16011  iprodclim3  16036  iprodmul  16039  ef0lem  16114  fprodefsum  16131  rpnnen2lem3  16252  dvdsflip  16354  fzo0dvdseq  16360  bitsinv1  16479  smupval  16525  smueqlem  16527  seq1st  16608  algr0  16609  prmind2  16722  crth  16815  eulerthlem2  16819  prmdiv  16822  pockthlem  16943  pockthg  16944  unbenlem  16946  prmunb  16952  prmgaplem7  17095  strfv2d  17238  imasvscaval  17583  oppccatid  17762  oppccatf  17771  epii  17787  fthepi  17975  funcestrcsetclem3  18187  funcsetcestrclem3  18201  yon12  18310  yon2  18311  yonedalem4c  18322  yonedalem22  18323  yonedalem3b  18324  yonedainv  18326  acsmapd  18599  mgm2nsgrplem1  18931  mgm2nsgrplem2  18932  mgm2nsgrplem3  18933  sgrp2nmndlem1  18936  sgrp2rid2  18939  ghmqusker  19305  cntrsubgnsg  19361  symgpssefmnd  19413  pmtrrn  19475  gexcl3  19605  efgi  19737  efgi2  19743  efgs1b  19754  efgredlemg  19760  efgredlemd  19762  frgpnabllem1  19891  cycsubgcyg  19919  gsumzaddlem  19939  dprdwd  20031  dprd2da  20062  rhmopp  20509  lsppratlem3  21151  lsppratlem4  21152  lbsextlem2  21161  lidl0ALT  21238  lidl1ALT  21241  2idl0  21270  2idl1  21271  domnchr  21547  znf1o  21570  mplsubrglem  22024  mpfconst  22125  mpfproj  22126  mpfind  22131  mhpmulcl  22153  pf1const  22350  pf1id  22351  mpfpf1  22355  pf1mpf  22356  madetsumid  22467  slesolex  22688  pmatcoe1fsupp  22707  mat2pmatbas0  22733  pmatcollpw  22787  pm2mpf1  22805  isclo  23095  indiscld  23099  restntr  23190  ordtbaslem  23196  ordtbas2  23199  lmconst  23269  lmss  23306  conncompid  23439  2ndcomap  23466  locfincmp  23534  comppfsc  23540  xkouni  23607  txcls  23612  ptclsg  23623  uptx  23633  txindis  23642  tx1stc  23658  cnmpt1res  23684  tgqtop  23720  uffix  23929  cnpflf2  24008  ptcmplem2  24061  ptcmplem4  24063  tgpconncomp  24121  tsmsfbas  24136  fmucnd  24301  prdsxmetlem  24378  imasdsf1olem  24383  prdsbl  24504  blcvx  24819  xrsmopn  24834  xrge0tsms  24856  metdcn2  24861  expcncf  24953  cnmpopc  24955  icchmeo  24971  icchmeoOLD  24972  iccpnfhmeo  24976  cnheibor  24987  evth  24991  evth2  24992  lebnumlem2  24994  lebnumii  24998  reparphti  25029  reparphtiOLD  25030  cfilfcls  25308  minveclem2  25460  minveclem3  25463  minveclem4  25466  ovoliunlem1  25537  ovolicc1  25551  iundisj  25583  volsup  25591  uniioombllem3  25620  vitalilem2  25644  vitalilem3  25645  mbfsup  25699  mbfinf  25700  mbflimsup  25701  itg2monolem1  25785  limcflflem  25915  limccnp  25926  limccnp2  25927  dvidlem  25950  dvn2bss  25966  cpnres  25973  dvcobr  25983  dvcobrOLD  25984  dvrec  25993  c1liplem1  26035  dvcnvrelem2  26057  dvfsumrlimf  26065  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsumrlim  26072  dvfsum2  26075  coeeulem  26263  coeid3  26279  plycn  26300  plycnOLD  26301  dvntaylp  26413  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulm2  26428  ulmshftlem  26432  ulmshft  26433  ulm0  26434  ulmcn  26442  ulmdvlem3  26445  ulmdv  26446  mtest  26447  mtestbdd  26448  dvradcnv  26464  psercn2  26466  psercn2OLD  26467  psercn  26470  pserdv  26473  abelth  26485  efif1olem2  26585  efif1olem4  26587  efifo  26589  eff1olem  26590  logcn  26689  dvloglem  26690  cxpcn3  26791  resqrtcn  26792  sqrtcn  26793  logbleb  26826  logblt  26827  asinneg  26929  atanlogsub  26959  atanbnd  26969  ressatans  26977  leibpilem2  26984  xrlimcnp  27011  efrlim  27012  efrlimOLD  27013  scvxcvx  27029  ppiub  27248  chtub  27256  logexprlim  27269  lgseisenlem1  27419  rplogsumlem1  27528  rplogsumlem2  27529  dchrisumlem2  27534  dchrisum0flb  27554  logdivbnd  27600  pntlem3  27653  dfnns2  28362  tgcgr4  28539  ltgov  28605  f1otrg  28879  eengtrkg  29001  iedgedg  29067  ushgredgedgloop  29248  subgruhgredgd  29301  uvtxupgrres  29425  umgr2v2evd2  29545  edginwlk  29653  wlk1walk  29657  crctcshwlkn0lem6  29835  wlkiswwlks1  29887  minvecolem1  30893  minvecolem2  30894  minvecolem4  30899  htthlem  30936  5oalem2  31674  3oalem2  31682  iundisjf  32602  fmptco1f1o  32643  xppreima  32655  xppreima2  32661  dfcnv2  32686  ccatws1f1o  32936  chnub  33002  chnccats1  33005  gsumhashmul  33064  xrge0tsmsd  33065  gsumwrd2dccatlem  33069  odpmco  33106  pmtrcnelor  33111  fzo0pmtrlast  33112  wrdpmtrlast  33113  pmtrto1cl  33119  psgnfzto1stlem  33120  fzto1stfv1  33121  fzto1st  33123  fzto1stinvn  33124  psgnfzto1st  33125  tocycf  33137  cycpmco2lem7  33152  cycpmco2  33153  cycpmrn  33163  cyc3evpm  33170  cyc3genpmlem  33171  cycpmgcl  33173  cyc3conja  33177  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspnsubrunlem1  33251  nsgmgc  33440  nsgqusf1olem1  33441  nsgqusf1olem2  33442  rhmpreimaprmidl  33479  ssdifidllem  33484  ssdifidl  33485  ssmxidllem  33501  drngmxidlr  33506  opprqus1r  33520  qsdrngilem  33522  qsdrngi  33523  rsprprmprmidlb  33551  rprmirredb  33560  1arithufdlem1  33572  1arithufdlem2  33573  1arithufdlem3  33574  1arithufdlem4  33575  fply1  33584  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  ply1degltdimlem  33673  ply1degltdim  33674  algextdeglem4  33761  algextdeglem6  33763  algextdeglem7  33764  algextdeglem8  33765  smatlem  33796  smatcl  33801  zartopn  33874  zarmxt1  33879  tpr2rico  33911  xrmulc1cn  33929  xrge0mulc1cn  33940  esumpfinvallem  34075  ldgenpisyslem1  34164  dynkin  34168  brfae  34249  sxbrsigalem3  34274  dya2icoseg2  34280  omsmeas  34325  sibfof  34342  sseqmw  34393  sseqf  34394  sseqp1  34397  fiblem  34400  fibp1  34403  probfinmeasbALTV  34431  repr0  34626  reprpmtf1o  34641  hgt750lemg  34669  bnj1379  34844  srcmpltd  35094  subfacp1lem5  35189  subfacp1lem6  35190  cvxpconn  35247  cvxsconn  35248  cvmliftlem6  35295  cvmliftlem8  35297  cvmliftlem10  35299  cvmlift2lem6  35313  cvmlift2lem11  35318  cvmlift2lem12  35319  2goelgoanfmla1  35429  prv1n  35436  msubff  35535  msubco  35536  elmsta  35553  msubff1  35561  mvhf  35563  msubvrs  35565  iprodefisumlem  35740  filnetlem3  36381  knoppcnlem10  36503  knoppcnlem11  36504  icoreunrn  37360  icoreelrn  37362  ralssiun  37408  poimirlem3  37630  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem30  37657  dvasin  37711  cover2  37722  upixp  37736  sdclem1  37750  fdc  37752  caushft  37768  ismtyres  37815  rrncmslem  37839  isfld2  38012  osumcllem10N  39967  pexmidlem7N  39978  dihglblem2N  41296  lcfrvalsnN  41543  lcfrlem5  41548  lcfrlem6  41549  lcfrlem27  41571  lcfrlem37  41581  aks6d1c1p4  42112  aks6d1c1p7  42114  aks6d1c1p8  42116  evl1gprodd  42118  aks6d1c2lem4  42128  aks6d1c5lem3  42138  aks6d1c6lem2  42172  prjspvs  42620  0prjspnrel  42637  monotuz  42953  expdiophlem1  43033  kelac2  43077  naddwordnexlem4  43414  grurankcld  44252  dvgrat  44331  nzss  44336  uzmptshftfval  44365  binomcxplemnotnn0  44375  refsumcn  45035  rfcnpre2  45036  rfcnpre3  45038  rfcnpre4  45039  disjf1o  45196  unirnmap  45213  unirnmapsn  45219  ssmapsn  45221  mptssid  45247  allbutfi  45404  eluzd  45420  uzidd2  45427  ressiocsup  45567  ressioosup  45568  ressiooinf  45570  fsumsermpt  45594  climexp  45620  climinf  45621  climsuse  45623  sumnnodd  45645  limsupresico  45715  limsupubuzlem  45727  limsupresxr  45781  liminfresxr  45782  liminfresico  45786  limsup10exlem  45787  cnrefiisplem  45844  cncfiooicclem1  45908  dvsinax  45928  itgsinexplem1  45969  fvvolioof  46004  fvvolicof  46006  stoweidlem14  46029  stoweidlem16  46031  stoweidlem31  46046  stoweidlem34  46049  stoweidlem36  46051  stoweidlem43  46058  stoweidlem46  46061  stoweidlem47  46062  stoweidlem52  46067  stoweidlem55  46070  stoweidlem57  46072  dirkercncf  46122  fourierdlem20  46142  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem54  46175  fourierdlem62  46183  fourierdlem71  46192  fourierdlem80  46201  fourierdlem114  46235  fouriersw  46246  ioorrnopnlem  46319  ioorrnopnxrlem  46321  salexct3  46357  salgencntex  46358  salgensscntex  46359  subsalsal  46374  sge0fodjrnlem  46431  sge0isum  46442  sge0seq  46461  sge0reuz  46462  sge0reuzb  46463  meadjiunlem  46480  meaiininclem  46501  carageniuncllem1  46536  caratheodorylem1  46541  hoiprodp1  46603  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  voncmpl  46636  hoiqssbl  46640  smflimlem2  46787  smfsuplem1  46826  smfsuplem3  46828  fsupdm  46857  finfdm  46861  cfsetsnfsetf  47070  fcores  47079  afvres  47184  afv2res  47251  fundcmpsurinjimaid  47398  iccpartigtl  47410  sprsymrelf  47482  prproropf1olem2  47491  isuspgrim0lem  47871  isuspgrimlem  47874  ushggricedg  47896  grimedg  47903  usgrgrtrirex  47917  isubgr3stgrlem7  47939  uspgrlimlem4  47958  gpgedgel  48007  gpg3kgrtriex  48045  funcringcsetcALTV2lem3  48208  funcringcsetclem3ALTV  48231  lindslinindsimp2lem5  48379  rrxsphere  48669  line2  48673  iooii  48815  icccldii  48816  iscnrm3rlem3  48839  oppcup  48948  onsetreclem3  49226  amgmwlem  49321