Theorem eleqtrrdi 2855

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  3eltr4g  2861  brelrng  5966  elabrex  7279  elabrexg  7280  fliftel1  7346  ovidig  7592  unielxp  8068  tfrlem11  8444  rdglim  8482  seqomlem4  8509  2oconcl  8559  ecopqsi  8832  erov  8872  eroprf  8873  sbthlem2  9150  dffi3  9500  ixpiunwdom  9659  cantnfcl  9736  r1lim  9841  rankwflemb  9862  pwwf  9876  unwf  9879  rankwflem  9884  uniwf  9888  rankpwi  9892  rankr1g  9901  r1pw  9914  r1rankid  9928  rankuni  9932  djulcl  9979  djurcl  9980  inlresf  9983  inrresf  9985  djuun  9995  cardlim  10041  infxpenlem  10082  alephfp  10177  cfsmolem  10339  alephsing  10345  hsmexlem4  10498  axdc3lem2  10520  numth3  10539  iunfo  10608  konigthlem  10637  iunctb  10643  canthwelem  10719  canthwe  10720  r1limwun  10805  inar1  10844  inatsk  10847  gruina  10887  grur1  10889  tskmval  10908  tskmcl  10910  pinq  10996  dmrecnq  11037  addclsr  11152  mulclsr  11153  axaddf  11214  axmulf  11215  peano2nn  12305  uztrn2  12922  eluz2nn  12949  peano2uzs  12967  uzsupss  13005  uzsup  13914  uzrdgfni  14009  uzrdgsuci  14011  fsuppmapnn0fiub  14042  seqf  14074  ser0  14105  bcm1k  14364  bcp1nk  14366  bcpasc  14370  hashprdifel  14447  fz1isolem  14510  pr2pwpr  14528  tpf  14548  ccats1val2  14675  rexuzre  15401  limsupgre  15527  climconst  15589  rlimclim1  15591  climrlim2  15593  clim2ser  15703  clim2ser2  15704  iserex  15705  isermulc2  15706  iserle  15708  isercolllem3  15715  isercoll2  15717  climsup  15718  iseraltlem2  15731  iseraltlem3  15732  zsum  15766  isumclim3  15807  isumadd  15815  fsump1i  15817  iserabs  15863  cvgcmp  15864  cvgcmpub  15865  cvgcmpce  15866  abscvgcvg  15867  isumshft  15887  isumsplit  15888  isum1p  15889  isumrpcl  15891  isumsup2  15894  climcndslem1  15897  cvgrat  15931  clim2prod  15936  clim2div  15937  prodf1  15939  ntrivcvgn0  15946  ntrivcvgtail  15948  fprodntriv  15990  fprodabs  16022  fprodeq0  16023  iprodclim3  16048  iprodmul  16051  ef0lem  16126  fprodefsum  16143  rpnnen2lem3  16264  dvdsflip  16365  fzo0dvdseq  16371  bitsinv1  16488  smupval  16534  smueqlem  16536  seq1st  16618  algr0  16619  prmind2  16732  crth  16825  eulerthlem2  16829  prmdiv  16832  pockthlem  16952  pockthg  16953  unbenlem  16955  prmunb  16961  prmgaplem7  17104  strfv2d  17249  imasvscaval  17598  oppccatid  17779  oppccatf  17788  epii  17804  fthepi  17995  funcestrcsetclem3  18211  funcsetcestrclem3  18225  yon12  18335  yon2  18336  yonedalem4c  18347  yonedalem22  18348  yonedalem3b  18349  yonedainv  18351  acsmapd  18624  mgm2nsgrplem1  18953  mgm2nsgrplem2  18954  mgm2nsgrplem3  18955  sgrp2nmndlem1  18958  sgrp2rid2  18961  ghmqusker  19327  cntrsubgnsg  19383  symgpssefmnd  19437  pmtrrn  19499  gexcl3  19629  efgi  19761  efgi2  19767  efgs1b  19778  efgredlemg  19784  efgredlemd  19786  frgpnabllem1  19915  cycsubgcyg  19943  gsumzaddlem  19963  dprdwd  20055  dprd2da  20086  rhmopp  20535  lsppratlem3  21174  lsppratlem4  21175  lbsextlem2  21184  lidl0ALT  21261  lidl1ALT  21264  2idl0  21293  2idl1  21294  domnchr  21570  znf1o  21593  mplsubrglem  22047  mpfconst  22148  mpfproj  22149  mpfind  22154  mhpmulcl  22176  pf1const  22371  pf1id  22372  mpfpf1  22376  pf1mpf  22377  madetsumid  22488  slesolex  22709  pmatcoe1fsupp  22728  mat2pmatbas0  22754  pmatcollpw  22808  pm2mpf1  22826  isclo  23116  indiscld  23120  restntr  23211  ordtbaslem  23217  ordtbas2  23220  lmconst  23290  lmss  23327  conncompid  23460  2ndcomap  23487  locfincmp  23555  comppfsc  23561  xkouni  23628  txcls  23633  ptclsg  23644  uptx  23654  txindis  23663  tx1stc  23679  cnmpt1res  23705  tgqtop  23741  uffix  23950  cnpflf2  24029  ptcmplem2  24082  ptcmplem4  24084  tgpconncomp  24142  tsmsfbas  24157  fmucnd  24322  prdsxmetlem  24399  imasdsf1olem  24404  prdsbl  24525  blcvx  24839  xrsmopn  24853  xrge0tsms  24875  metdcn2  24880  expcncf  24972  cnmpopc  24974  icchmeo  24990  icchmeoOLD  24991  iccpnfhmeo  24995  cnheibor  25006  evth  25010  evth2  25011  lebnumlem2  25013  lebnumii  25017  reparphti  25048  reparphtiOLD  25049  cfilfcls  25327  minveclem2  25479  minveclem3  25482  minveclem4  25485  ovoliunlem1  25556  ovolicc1  25570  iundisj  25602  volsup  25610  uniioombllem3  25639  vitalilem2  25663  vitalilem3  25664  mbfsup  25718  mbfinf  25719  mbflimsup  25720  itg2monolem1  25805  limcflflem  25935  limccnp  25946  limccnp2  25947  dvidlem  25970  dvn2bss  25986  cpnres  25993  dvcobr  26003  dvcobrOLD  26004  dvrec  26013  c1liplem1  26055  dvcnvrelem2  26077  dvfsumrlimf  26085  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsumrlim  26092  dvfsum2  26095  coeeulem  26283  coeid3  26299  plycn  26320  plycnOLD  26321  dvntaylp  26431  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulm2  26446  ulmshftlem  26450  ulmshft  26451  ulm0  26452  ulmcn  26460  ulmdvlem3  26463  ulmdv  26464  mtest  26465  mtestbdd  26466  dvradcnv  26482  psercn2  26484  psercn2OLD  26485  psercn  26488  pserdv  26491  abelth  26503  efif1olem2  26603  efif1olem4  26605  efifo  26607  eff1olem  26608  logcn  26707  dvloglem  26708  cxpcn3  26809  resqrtcn  26810  sqrtcn  26811  logbleb  26844  logblt  26845  asinneg  26947  atanlogsub  26977  atanbnd  26987  ressatans  26995  leibpilem2  27002  xrlimcnp  27029  efrlim  27030  efrlimOLD  27031  scvxcvx  27047  ppiub  27266  chtub  27274  logexprlim  27287  lgseisenlem1  27437  rplogsumlem1  27546  rplogsumlem2  27547  dchrisumlem2  27552  dchrisum0flb  27572  logdivbnd  27618  pntlem3  27671  dfnns2  28380  tgcgr4  28557  ltgov  28623  f1otrg  28897  eengtrkg  29019  iedgedg  29085  ushgredgedgloop  29266  subgruhgredgd  29319  uvtxupgrres  29443  umgr2v2evd2  29563  edginwlk  29671  wlk1walk  29675  crctcshwlkn0lem6  29848  wlkiswwlks1  29900  minvecolem1  30906  minvecolem2  30907  minvecolem4  30912  htthlem  30949  5oalem2  31687  3oalem2  31695  iundisjf  32611  fmptco1f1o  32652  xppreima  32664  xppreima2  32669  dfcnv2  32694  ccatws1f1o  32918  chnub  32984  gsumhashmul  33040  xrge0tsmsd  33041  odpmco  33079  pmtrcnelor  33084  fzo0pmtrlast  33085  wrdpmtrlast  33086  pmtrto1cl  33092  psgnfzto1stlem  33093  fzto1stfv1  33094  fzto1st  33096  fzto1stinvn  33097  psgnfzto1st  33098  tocycf  33110  cycpmco2lem7  33125  cycpmco2  33126  cycpmrn  33136  cyc3evpm  33143  cyc3genpmlem  33144  cycpmgcl  33146  cyc3conja  33150  nsgmgc  33405  nsgqusf1olem1  33406  nsgqusf1olem2  33407  rhmpreimaprmidl  33444  ssdifidllem  33449  ssdifidl  33450  ssmxidllem  33466  drngmxidlr  33471  opprqus1r  33485  qsdrngilem  33487  qsdrngi  33488  rsprprmprmidlb  33516  rprmirredb  33525  1arithufdlem1  33537  1arithufdlem2  33538  1arithufdlem3  33539  1arithufdlem4  33540  fply1  33549  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  ply1degltdimlem  33635  ply1degltdim  33636  algextdeglem4  33711  algextdeglem6  33713  algextdeglem7  33714  algextdeglem8  33715  smatlem  33743  smatcl  33748  zartopn  33821  zarmxt1  33826  tpr2rico  33858  xrmulc1cn  33876  xrge0mulc1cn  33887  esumpfinvallem  34038  ldgenpisyslem1  34127  dynkin  34131  brfae  34212  sxbrsigalem3  34237  dya2icoseg2  34243  omsmeas  34288  sibfof  34305  sseqmw  34356  sseqf  34357  sseqp1  34360  fiblem  34363  fibp1  34366  probfinmeasbALTV  34394  repr0  34588  reprpmtf1o  34603  hgt750lemg  34631  bnj1379  34806  srcmpltd  35056  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  35702  filnetlem3  36346  knoppcnlem10  36468  knoppcnlem11  36469  icoreunrn  37325  icoreelrn  37327  ralssiun  37373  poimirlem3  37583  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem30  37610  dvasin  37664  cover2  37675  upixp  37689  sdclem1  37703  fdc  37705  caushft  37721  ismtyres  37768  rrncmslem  37792  isfld2  37965  osumcllem10N  39922  pexmidlem7N  39933  dihglblem2N  41251  lcfrvalsnN  41498  lcfrlem5  41503  lcfrlem6  41504  lcfrlem27  41526  lcfrlem37  41536  aks6d1c1p4  42068  aks6d1c1p7  42070  aks6d1c1p8  42072  evl1gprodd  42074  aks6d1c2lem4  42084  aks6d1c5lem3  42094  aks6d1c6lem2  42128  prjspvs  42565  0prjspnrel  42582  monotuz  42898  expdiophlem1  42978  kelac2  43022  naddwordnexlem4  43363  grurankcld  44202  dvgrat  44281  nzss  44286  uzmptshftfval  44315  binomcxplemnotnn0  44325  refsumcn  44930  rfcnpre2  44931  rfcnpre3  44933  rfcnpre4  44934  disjf1o  45098  unirnmap  45115  unirnmapsn  45121  ssmapsn  45123  mptssid  45149  allbutfi  45308  eluzd  45324  uzidd2  45331  ressiocsup  45472  ressioosup  45473  ressiooinf  45475  fsumsermpt  45500  climexp  45526  climinf  45527  climsuse  45529  sumnnodd  45551  limsupresico  45621  limsupubuzlem  45633  limsupresxr  45687  liminfresxr  45688  liminfresico  45692  limsup10exlem  45693  cnrefiisplem  45750  cncfiooicclem1  45814  dvsinax  45834  itgsinexplem1  45875  fvvolioof  45910  fvvolicof  45912  stoweidlem14  45935  stoweidlem16  45937  stoweidlem31  45952  stoweidlem34  45955  stoweidlem36  45957  stoweidlem43  45964  stoweidlem46  45967  stoweidlem47  45968  stoweidlem52  45973  stoweidlem55  45976  stoweidlem57  45978  dirkercncf  46028  fourierdlem20  46048  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem54  46081  fourierdlem62  46089  fourierdlem71  46098  fourierdlem80  46107  fourierdlem114  46141  fouriersw  46152  ioorrnopnlem  46225  ioorrnopnxrlem  46227  salexct3  46263  salgencntex  46264  salgensscntex  46265  subsalsal  46280  sge0fodjrnlem  46337  sge0isum  46348  sge0seq  46367  sge0reuz  46368  sge0reuzb  46369  meadjiunlem  46386  meaiininclem  46407  carageniuncllem1  46442  caratheodorylem1  46447  hoiprodp1  46509  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  voncmpl  46542  hoiqssbl  46546  smflimlem2  46693  smfsuplem1  46732  smfsuplem3  46734  fsupdm  46763  finfdm  46767  cfsetsnfsetf  46973  fcores  46982  afvres  47087  afv2res  47154  fundcmpsurinjimaid  47285  iccpartigtl  47297  sprsymrelf  47369  prproropf1olem2  47378  isuspgrim0lem  47755  isuspgrimlem  47758  ushggricedg  47780  grimedg  47787  usgrgrtrirex  47799  uspgrlimlem4  47815  funcringcsetcALTV2lem3  48015  funcringcsetclem3ALTV  48038  lindslinindsimp2lem5  48191  rrxsphere  48482  line2  48486  iooii  48597  icccldii  48598  iscnrm3rlem3  48622  onsetreclem3  48799  amgmwlem  48896