Theorem eleqtrrdi 2842

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808

This theorem is referenced by:  3eltr4g  2848  brelrng  5939  elabrex  7243  elabrexg  7244  fliftel1  7309  ovidig  7552  unielxp  8015  tfrlem11  8390  rdglim  8428  seqomlem4  8455  2oconcl  8505  ecopqsi  8770  erov  8810  eroprf  8811  sbthlem2  9086  dffi3  9428  ixpiunwdom  9587  cantnfcl  9664  r1lim  9769  rankwflemb  9790  pwwf  9804  unwf  9807  rankwflem  9812  uniwf  9816  rankpwi  9820  rankr1g  9829  r1pw  9842  r1rankid  9856  rankuni  9860  djulcl  9907  djurcl  9908  inlresf  9911  inrresf  9913  djuun  9923  cardlim  9969  infxpenlem  10010  alephfp  10105  cfsmolem  10267  alephsing  10273  hsmexlem4  10426  axdc3lem2  10448  numth3  10467  iunfo  10536  konigthlem  10565  iunctb  10571  canthwelem  10647  canthwe  10648  r1limwun  10733  inar1  10772  inatsk  10775  gruina  10815  grur1  10817  tskmval  10836  tskmcl  10838  pinq  10924  dmrecnq  10965  addclsr  11080  mulclsr  11081  axaddf  11142  axmulf  11143  peano2nn  12228  uztrn2  12845  eluz2nn  12872  peano2uzs  12890  uzsupss  12928  uzsup  13832  uzrdgfni  13927  uzrdgsuci  13929  fsuppmapnn0fiub  13960  seqf  13993  ser0  14024  bcm1k  14279  bcp1nk  14281  bcpasc  14285  hashprdifel  14362  fz1isolem  14426  pr2pwpr  14444  ccats1val2  14581  rexuzre  15303  limsupgre  15429  climconst  15491  rlimclim1  15493  climrlim2  15495  clim2ser  15605  clim2ser2  15606  iserex  15607  isermulc2  15608  iserle  15610  isercolllem3  15617  isercoll2  15619  climsup  15620  iseraltlem2  15633  iseraltlem3  15634  zsum  15668  isumclim3  15709  isumadd  15717  fsump1i  15719  iserabs  15765  cvgcmp  15766  cvgcmpub  15767  cvgcmpce  15768  abscvgcvg  15769  isumshft  15789  isumsplit  15790  isum1p  15791  isumrpcl  15793  isumsup2  15796  climcndslem1  15799  cvgrat  15833  clim2prod  15838  clim2div  15839  prodf1  15841  ntrivcvgn0  15848  ntrivcvgtail  15850  fprodntriv  15890  fprodabs  15922  fprodeq0  15923  iprodclim3  15948  iprodmul  15951  ef0lem  16026  fprodefsum  16042  rpnnen2lem3  16163  dvdsflip  16264  fzo0dvdseq  16270  bitsinv1  16387  smupval  16433  smueqlem  16435  seq1st  16512  algr0  16513  prmind2  16626  crth  16715  eulerthlem2  16719  prmdiv  16722  pockthlem  16842  pockthg  16843  unbenlem  16845  prmunb  16851  prmgaplem7  16994  strfv2d  17139  imasvscaval  17488  oppccatid  17669  oppccatf  17678  epii  17694  fthepi  17883  funcestrcsetclem3  18098  funcsetcestrclem3  18112  yon12  18222  yon2  18223  yonedalem4c  18234  yonedalem22  18235  yonedalem3b  18236  yonedainv  18238  acsmapd  18511  mgm2nsgrplem1  18835  mgm2nsgrplem2  18836  mgm2nsgrplem3  18837  sgrp2nmndlem1  18840  sgrp2rid2  18843  cntrsubgnsg  19248  symgpssefmnd  19304  pmtrrn  19366  gexcl3  19496  efgi  19628  efgi2  19634  efgs1b  19645  efgredlemg  19651  efgredlemd  19653  frgpnabllem1  19782  cycsubgcyg  19810  gsumzaddlem  19830  dprdwd  19922  dprd2da  19953  rhmopp  20400  lsppratlem3  20907  lsppratlem4  20908  lbsextlem2  20917  lidl0  20993  lidl1  20994  2idl0  21012  2idl1  21013  domnchr  21303  znf1o  21326  mplsubrglem  21782  mpfconst  21883  mpfproj  21884  mpfind  21889  mhpmulcl  21911  pf1const  22085  pf1id  22086  mpfpf1  22090  pf1mpf  22091  madetsumid  22183  slesolex  22404  pmatcoe1fsupp  22423  mat2pmatbas0  22449  pmatcollpw  22503  pm2mpf1  22521  isclo  22811  indiscld  22815  restntr  22906  ordtbaslem  22912  ordtbas2  22915  lmconst  22985  lmss  23022  conncompid  23155  2ndcomap  23182  locfincmp  23250  comppfsc  23256  xkouni  23323  txcls  23328  ptclsg  23339  uptx  23349  txindis  23358  tx1stc  23374  cnmpt1res  23400  tgqtop  23436  uffix  23645  cnpflf2  23724  ptcmplem2  23777  ptcmplem4  23779  tgpconncomp  23837  tsmsfbas  23852  fmucnd  24017  prdsxmetlem  24094  imasdsf1olem  24099  prdsbl  24220  blcvx  24534  xrsmopn  24548  xrge0tsms  24570  metdcn2  24575  expcncf  24667  cnmpopc  24669  icchmeo  24685  icchmeoOLD  24686  iccpnfhmeo  24690  cnheibor  24701  evth  24705  evth2  24706  lebnumlem2  24708  lebnumii  24712  reparphti  24743  reparphtiOLD  24744  cfilfcls  25022  minveclem2  25174  minveclem3  25177  minveclem4  25180  ovoliunlem1  25251  ovolicc1  25265  iundisj  25297  volsup  25305  uniioombllem3  25334  vitalilem2  25358  vitalilem3  25359  mbfsup  25413  mbfinf  25414  mbflimsup  25415  itg2monolem1  25500  limcflflem  25629  limccnp  25640  limccnp2  25641  dvidlem  25664  dvn2bss  25680  cpnres  25687  dvcobr  25697  dvcobrOLD  25698  dvrec  25707  c1liplem1  25748  dvcnvrelem2  25770  dvfsumrlimf  25777  dvfsumlem1  25778  dvfsumlem2  25779  dvfsumlem3  25780  dvfsumlem4  25781  dvfsumrlim  25783  dvfsum2  25786  coeeulem  25973  coeid3  25989  plycn  26010  plycnOLD  26011  dvntaylp  26119  taylthlem1  26121  taylthlem2  26122  ulm2  26133  ulmshftlem  26137  ulmshft  26138  ulm0  26139  ulmcn  26147  ulmdvlem3  26150  ulmdv  26151  mtest  26152  mtestbdd  26153  dvradcnv  26169  psercn2  26171  psercn  26174  pserdv  26177  abelth  26189  efif1olem2  26288  efif1olem4  26290  efifo  26292  eff1olem  26293  logcn  26391  dvloglem  26392  cxpcn3  26492  resqrtcn  26493  sqrtcn  26494  logbleb  26524  logblt  26525  asinneg  26627  atanlogsub  26657  atanbnd  26667  ressatans  26675  leibpilem2  26682  xrlimcnp  26709  efrlim  26710  scvxcvx  26726  ppiub  26943  chtub  26951  logexprlim  26964  lgseisenlem1  27114  rplogsumlem1  27223  rplogsumlem2  27224  dchrisumlem2  27229  dchrisum0flb  27249  logdivbnd  27295  pntlem3  27348  peano2n0s  27940  tgcgr4  28049  ltgov  28115  f1otrg  28389  eengtrkg  28511  iedgedg  28577  ushgredgedgloop  28755  subgruhgredgd  28808  uvtxupgrres  28932  umgr2v2evd2  29051  edginwlk  29159  wlk1walk  29163  crctcshwlkn0lem6  29336  wlkiswwlks1  29388  minvecolem1  30394  minvecolem2  30395  minvecolem4  30400  htthlem  30437  5oalem2  31175  3oalem2  31183  iundisjf  32087  fmptco1f1o  32124  xppreima  32138  xppreima2  32143  dfcnv2  32168  gsumhashmul  32478  xrge0tsmsd  32479  odpmco  32517  pmtrcnelor  32522  pmtrto1cl  32528  psgnfzto1stlem  32529  fzto1stfv1  32530  fzto1st  32532  fzto1stinvn  32533  psgnfzto1st  32534  tocycf  32546  cycpmco2lem7  32561  cycpmco2  32562  cycpmrn  32572  cyc3evpm  32579  cyc3genpmlem  32580  cycpmgcl  32582  cyc3conja  32586  nsgmgc  32797  nsgqusf1olem1  32798  nsgqusf1olem2  32799  ghmqusker  32806  rhmpreimaprmidl  32844  ssmxidllem  32863  opprqus1r  32880  qsdrngilem  32882  qsdrngi  32883  fply1  32911  ply1degltel  32940  ply1degleel  32941  ply1degltlss  32942  ply1degltdimlem  32995  ply1degltdim  32996  algextdeglem4  33065  algextdeglem6  33067  algextdeglem7  33068  algextdeglem8  33069  smatlem  33075  smatcl  33080  zartopn  33153  zarmxt1  33158  tpr2rico  33190  xrmulc1cn  33208  xrge0mulc1cn  33219  esumpfinvallem  33370  ldgenpisyslem1  33459  dynkin  33463  brfae  33544  sxbrsigalem3  33569  dya2icoseg2  33575  omsmeas  33620  sibfof  33637  sseqmw  33688  sseqf  33689  sseqp1  33692  fiblem  33695  fibp1  33698  probfinmeasbALTV  33726  repr0  33921  reprpmtf1o  33936  hgt750lemg  33964  bnj1379  34139  srcmpltd  34383  subfacp1lem5  34473  subfacp1lem6  34474  cvxpconn  34531  cvxsconn  34532  cvmliftlem6  34579  cvmliftlem8  34581  cvmliftlem10  34583  cvmlift2lem6  34597  cvmlift2lem11  34602  cvmlift2lem12  34603  2goelgoanfmla1  34713  prv1n  34720  msubff  34819  msubco  34820  elmsta  34837  msubff1  34845  mvhf  34847  msubvrs  34849  iprodefisumlem  35014  gg-psercn2  35464  gg-dvfsumlem2  35469  filnetlem3  35568  knoppcnlem10  35681  knoppcnlem11  35682  icoreunrn  36543  icoreelrn  36545  ralssiun  36591  poimirlem3  36794  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem30  36821  dvasin  36875  cover2  36886  upixp  36900  sdclem1  36914  fdc  36916  caushft  36932  ismtyres  36979  rrncmslem  37003  isfld2  37176  osumcllem10N  39139  pexmidlem7N  39150  dihglblem2N  40468  lcfrvalsnN  40715  lcfrlem5  40720  lcfrlem6  40721  lcfrlem27  40743  lcfrlem37  40753  prjspvs  41654  0prjspnrel  41671  monotuz  41982  expdiophlem1  42062  kelac2  42109  naddwordnexlem4  42454  grurankcld  43294  dvgrat  43373  nzss  43378  uzmptshftfval  43407  binomcxplemnotnn0  43417  refsumcn  44016  rfcnpre2  44017  rfcnpre3  44019  rfcnpre4  44020  disjf1o  44188  unirnmap  44205  unirnmapsn  44211  ssmapsn  44213  mptssid  44242  allbutfi  44401  eluzd  44417  uzidd2  44424  ressiocsup  44565  ressioosup  44566  ressiooinf  44568  fsumsermpt  44593  climexp  44619  climinf  44620  climsuse  44622  sumnnodd  44644  limsupresico  44714  limsupubuzlem  44726  limsupresxr  44780  liminfresxr  44781  liminfresico  44785  limsup10exlem  44786  cnrefiisplem  44843  cncfiooicclem1  44907  dvsinax  44927  itgsinexplem1  44968  fvvolioof  45003  fvvolicof  45005  stoweidlem14  45028  stoweidlem16  45030  stoweidlem31  45045  stoweidlem34  45048  stoweidlem36  45050  stoweidlem43  45057  stoweidlem46  45060  stoweidlem47  45061  stoweidlem52  45066  stoweidlem55  45069  stoweidlem57  45071  dirkercncf  45121  fourierdlem20  45141  fourierdlem42  45163  fourierdlem48  45168  fourierdlem49  45169  fourierdlem51  45171  fourierdlem54  45174  fourierdlem62  45182  fourierdlem71  45191  fourierdlem80  45200  fourierdlem114  45234  fouriersw  45245  ioorrnopnlem  45318  ioorrnopnxrlem  45320  salexct3  45356  salgencntex  45357  salgensscntex  45358  subsalsal  45373  sge0fodjrnlem  45430  sge0isum  45441  sge0seq  45460  sge0reuz  45461  sge0reuzb  45462  meadjiunlem  45479  meaiininclem  45500  carageniuncllem1  45535  caratheodorylem1  45540  hoiprodp1  45602  hoidmv1lelem1  45605  hoidmv1lelem2  45606  hoidmv1le  45608  hoidmvlelem1  45609  hoidmvlelem2  45610  hoidmvlelem3  45611  voncmpl  45635  hoiqssbl  45639  smflimlem2  45786  smfsuplem1  45825  smfsuplem3  45827  fsupdm  45856  finfdm  45860  cfsetsnfsetf  46066  fcores  46075  afvres  46178  afv2res  46245  fundcmpsurinjimaid  46377  iccpartigtl  46389  sprsymrelf  46461  prproropf1olem2  46470  ushrisomgr  46807  funcringcsetcALTV2lem3  47024  funcringcsetclem3ALTV  47047  lindslinindsimp2lem5  47230  rrxsphere  47521  line2  47525  iooii  47637  icccldii  47638  iscnrm3rlem3  47662  onsetreclem3  47839  amgmwlem  47936