Theorem eleqtrrdi 2847

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  3eltr4g  2853  brelrng  5896  elabrex  7197  elabrexg  7198  fliftel1  7265  ovidig  7509  unielxp  7980  tfrlem11  8327  rdglim  8365  seqomlem4  8392  2oconcl  8438  ecopqsi  8717  erov  8761  eroprf  8762  sbthlem2  9026  dffi3  9344  ixpiunwdom  9505  cantnfcl  9588  r1lim  9696  rankwflemb  9717  pwwf  9731  unwf  9734  rankwflem  9739  uniwf  9743  rankpwi  9747  rankr1g  9756  r1pw  9769  r1rankid  9783  rankuni  9787  djulcl  9834  djurcl  9835  inlresf  9838  inrresf  9840  djuun  9850  cardlim  9896  infxpenlem  9935  alephfp  10030  cfsmolem  10192  alephsing  10198  hsmexlem4  10351  axdc3lem2  10373  numth3  10392  iunfo  10461  konigthlem  10491  iunctb  10497  canthwelem  10573  canthwe  10574  r1limwun  10659  inar1  10698  inatsk  10701  gruina  10741  grur1  10743  tskmval  10762  tskmcl  10764  pinq  10850  dmrecnq  10891  addclsr  11006  mulclsr  11007  axaddf  11068  axmulf  11069  peano2nn  12186  uztrn2  12807  eluz2nn  12838  peano2uzs  12852  uzsupss  12890  uzsup  13822  uzrdgfni  13920  uzrdgsuci  13922  fsuppmapnn0fiub  13953  seqf  13985  ser0  14016  bcm1k  14277  bcp1nk  14279  bcpasc  14283  hashprdifel  14360  fz1isolem  14423  pr2pwpr  14441  tpf  14461  ccats1val2  14590  rexuzre  15315  limsupgre  15443  climconst  15505  rlimclim1  15507  climrlim2  15509  clim2ser  15617  clim2ser2  15618  iserex  15619  isermulc2  15620  iserle  15622  isercolllem3  15629  isercoll2  15631  climsup  15632  iseraltlem2  15645  iseraltlem3  15646  zsum  15680  isumclim3  15721  isumadd  15729  fsump1i  15731  iserabs  15778  cvgcmp  15779  cvgcmpub  15780  cvgcmpce  15781  abscvgcvg  15782  isumshft  15804  isumsplit  15805  isum1p  15806  isumrpcl  15808  isumsup2  15811  climcndslem1  15814  cvgrat  15848  clim2prod  15853  clim2div  15854  prodf1  15856  ntrivcvgn0  15863  ntrivcvgtail  15865  fprodntriv  15907  fprodabs  15939  fprodeq0  15940  iprodclim3  15965  iprodmul  15968  ef0lem  16043  fprodefsum  16060  rpnnen2lem3  16183  dvdsflip  16286  fzo0dvdseq  16292  bitsinv1  16411  smupval  16457  smueqlem  16459  seq1st  16540  algr0  16541  prmind2  16654  crth  16748  eulerthlem2  16752  prmdiv  16755  pockthlem  16876  pockthg  16877  unbenlem  16879  prmunb  16885  prmgaplem7  17028  strfv2d  17171  imasvscaval  17502  oppccatid  17685  oppccatf  17694  epii  17710  fthepi  17897  funcestrcsetclem3  18108  funcsetcestrclem3  18122  yon12  18231  yon2  18232  yonedalem4c  18243  yonedalem22  18244  yonedalem3b  18245  yonedainv  18247  acsmapd  18520  chnub  18588  chnccats1  18591  chnccat  18592  mgm2nsgrplem1  18889  mgm2nsgrplem2  18890  mgm2nsgrplem3  18891  sgrp2nmndlem1  18894  sgrp2rid2  18897  ghmqusker  19262  cntrsubgnsg  19318  symgpssefmnd  19371  pmtrrn  19432  gexcl3  19562  efgi  19694  efgi2  19700  efgs1b  19711  efgredlemg  19717  efgredlemd  19719  frgpnabllem1  19848  cycsubgcyg  19876  gsumzaddlem  19896  dprdwd  19988  dprd2da  20019  rhmopp  20486  lsppratlem3  21147  lsppratlem4  21148  lbsextlem2  21157  lidl0ALT  21226  lidl1ALT  21229  2idl0  21258  2idl1  21259  domnchr  21512  znf1o  21531  mplsubrglem  21982  mpfconst  22087  mpfproj  22088  mpfind  22093  mhpmulcl  22115  pf1const  22311  pf1id  22312  mpfpf1  22316  pf1mpf  22317  madetsumid  22426  slesolex  22647  pmatcoe1fsupp  22666  mat2pmatbas0  22692  pmatcollpw  22746  pm2mpf1  22764  isclo  23052  indiscld  23056  restntr  23147  ordtbaslem  23153  ordtbas2  23156  lmconst  23226  lmss  23263  conncompid  23396  2ndcomap  23423  locfincmp  23491  comppfsc  23497  xkouni  23564  txcls  23569  ptclsg  23580  uptx  23590  txindis  23599  tx1stc  23615  cnmpt1res  23641  tgqtop  23677  uffix  23886  cnpflf2  23965  ptcmplem2  24018  ptcmplem4  24020  tgpconncomp  24078  tsmsfbas  24093  fmucnd  24256  prdsxmetlem  24333  imasdsf1olem  24338  prdsbl  24456  blcvx  24763  xrsmopn  24778  xrge0tsms  24800  metdcn2  24805  expcncf  24893  cnmpopc  24895  icchmeo  24908  iccpnfhmeo  24912  cnheibor  24922  evth  24926  evth2  24927  lebnumlem2  24929  lebnumii  24933  reparphti  24964  cfilfcls  25241  minveclem2  25393  minveclem3  25396  minveclem4  25399  ovoliunlem1  25469  ovolicc1  25483  iundisj  25515  volsup  25523  uniioombllem3  25552  vitalilem2  25576  vitalilem3  25577  mbfsup  25631  mbfinf  25632  mbflimsup  25633  itg2monolem1  25717  limcflflem  25847  limccnp  25858  limccnp2  25859  dvidlem  25882  dvn2bss  25897  cpnres  25904  dvcobr  25913  dvrec  25922  c1liplem1  25963  dvcnvrelem2  25985  dvfsumrlimf  25992  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlim  25998  dvfsum2  26001  coeeulem  26189  coeid3  26205  plycn  26226  dvntaylp  26336  taylthlem1  26338  taylthlem2  26339  ulm2  26350  ulmshftlem  26354  ulmshft  26355  ulm0  26356  ulmcn  26364  ulmdvlem3  26367  ulmdv  26368  mtest  26369  mtestbdd  26370  dvradcnv  26386  psercn2  26388  psercn  26391  pserdv  26394  abelth  26406  efif1olem2  26507  efif1olem4  26509  efifo  26511  eff1olem  26512  logcn  26611  dvloglem  26612  cxpcn3  26712  resqrtcn  26713  sqrtcn  26714  logbleb  26747  logblt  26748  asinneg  26850  atanlogsub  26880  atanbnd  26890  ressatans  26898  leibpilem2  26905  xrlimcnp  26932  efrlim  26933  scvxcvx  26949  ppiub  27167  chtub  27175  logexprlim  27188  lgseisenlem1  27338  rplogsumlem1  27447  rplogsumlem2  27448  dchrisumlem2  27453  dchrisum0flb  27473  logdivbnd  27519  pntlem3  27572  dfnns2  28364  tgcgr4  28599  ltgov  28665  f1otrg  28939  eengtrkg  29055  iedgedg  29119  ushgredgedgloop  29300  subgruhgredgd  29353  uvtxupgrres  29477  umgr2v2evd2  29596  edginwlk  29703  wlk1walk  29707  crctcshwlkn0lem6  29883  wlkiswwlks1  29935  minvecolem1  30945  minvecolem2  30946  minvecolem4  30951  htthlem  30988  5oalem2  31726  3oalem2  31734  iundisjf  32659  fmptco1f1o  32706  xppreima  32718  xppreima2  32724  dfcnv2  32748  ccatws1f1o  33011  gsumhashmul  33128  xrge0tsmsd  33134  gsumwrd2dccatlem  33138  odpmco  33147  pmtrcnelor  33152  fzo0pmtrlast  33153  wrdpmtrlast  33154  pmtrto1cl  33160  psgnfzto1stlem  33161  fzto1stfv1  33162  fzto1st  33164  fzto1stinvn  33165  psgnfzto1st  33166  tocycf  33178  cycpmco2lem7  33193  cycpmco2  33194  cycpmrn  33204  cyc3evpm  33211  cyc3genpmlem  33212  cycpmgcl  33214  cyc3conja  33218  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspnsubrunlem1  33308  nsgmgc  33472  nsgqusf1olem1  33473  nsgqusf1olem2  33474  rhmpreimaprmidl  33511  ssdifidllem  33516  ssdifidl  33517  ssmxidllem  33533  drngmxidlr  33538  opprqus1r  33552  qsdrngilem  33554  qsdrngi  33555  rsprprmprmidlb  33583  rprmirredb  33592  1arithufdlem1  33604  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  fply1  33618  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  mplmulmvr  33683  psrmon  33693  psrmonprod  33696  esplylem  33710  esplyfv1  33713  esplysply  33715  esplyind  33719  ply1degltdimlem  33766  ply1degltdim  33767  algextdeglem4  33864  algextdeglem6  33866  algextdeglem7  33867  algextdeglem8  33868  nn0constr  33905  smatlem  33941  smatcl  33946  zartopn  34019  zarmxt1  34024  tpr2rico  34056  xrmulc1cn  34074  xrge0mulc1cn  34085  esumpfinvallem  34218  ldgenpisyslem1  34307  dynkin  34311  brfae  34392  sxbrsigalem3  34416  dya2icoseg2  34422  omsmeas  34467  sibfof  34484  sseqmw  34535  sseqf  34536  sseqp1  34539  fiblem  34542  fibp1  34545  probfinmeasbALTV  34573  repr0  34755  reprpmtf1o  34770  hgt750lemg  34798  bnj1379  34972  srcmpltd  35222  fineqvnttrclselem3  35267  subfacp1lem5  35366  subfacp1lem6  35367  cvxpconn  35424  cvxsconn  35425  cvmliftlem6  35472  cvmliftlem8  35474  cvmliftlem10  35476  cvmlift2lem6  35490  cvmlift2lem11  35495  cvmlift2lem12  35496  2goelgoanfmla1  35606  prv1n  35613  msubff  35712  msubco  35713  elmsta  35730  msubff1  35738  mvhf  35740  msubvrs  35742  iprodefisumlem  35922  filnetlem3  36562  ttcid  36674  ttcwf  36706  knoppcnlem10  36762  knoppcnlem11  36763  icoreunrn  37675  icoreelrn  37677  ralssiun  37723  poimirlem3  37944  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem30  37971  dvasin  38025  cover2  38036  upixp  38050  sdclem1  38064  fdc  38066  caushft  38082  ismtyres  38129  rrncmslem  38153  isfld2  38326  presuc  38819  osumcllem10N  40411  pexmidlem7N  40422  dihglblem2N  41740  lcfrvalsnN  41987  lcfrlem5  41992  lcfrlem6  41993  lcfrlem27  42015  lcfrlem37  42025  aks6d1c1p4  42550  aks6d1c1p7  42552  aks6d1c1p8  42554  evl1gprodd  42556  aks6d1c2lem4  42566  aks6d1c5lem3  42576  aks6d1c6lem2  42610  prjspvs  43043  0prjspnrel  43060  monotuz  43369  expdiophlem1  43449  kelac2  43493  naddwordnexlem4  43829  grurankcld  44660  dvgrat  44739  nzss  44744  uzmptshftfval  44773  binomcxplemnotnn0  44783  orbitinit  45383  orbitcl  45384  permaxinf2lem  45439  refsumcn  45461  rfcnpre2  45462  rfcnpre3  45464  rfcnpre4  45465  disjf1o  45621  unirnmap  45637  unirnmapsn  45643  ssmapsn  45645  mptssid  45670  allbutfi  45822  eluzd  45837  uzidd2  45844  ressiocsup  45984  ressioosup  45985  ressiooinf  45987  fsumsermpt  46009  climexp  46035  climinf  46036  climsuse  46038  sumnnodd  46060  limsupresico  46128  limsupubuzlem  46140  limsupresxr  46194  liminfresxr  46195  liminfresico  46199  limsup10exlem  46200  cnrefiisplem  46257  cncfiooicclem1  46321  dvsinax  46341  itgsinexplem1  46382  fvvolioof  46417  fvvolicof  46419  stoweidlem14  46442  stoweidlem16  46444  stoweidlem31  46459  stoweidlem34  46462  stoweidlem36  46464  stoweidlem43  46471  stoweidlem46  46474  stoweidlem47  46475  stoweidlem52  46480  stoweidlem55  46483  stoweidlem57  46485  dirkercncf  46535  fourierdlem20  46555  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem54  46588  fourierdlem62  46596  fourierdlem71  46605  fourierdlem80  46614  fourierdlem114  46648  fouriersw  46659  ioorrnopnlem  46732  ioorrnopnxrlem  46734  salexct3  46770  salgencntex  46771  salgensscntex  46772  subsalsal  46787  sge0fodjrnlem  46844  sge0isum  46855  sge0seq  46874  sge0reuz  46875  sge0reuzb  46876  meadjiunlem  46893  meaiininclem  46914  carageniuncllem1  46949  caratheodorylem1  46954  hoiprodp1  47016  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  voncmpl  47049  hoiqssbl  47053  smflimlem2  47200  smfsuplem1  47239  smfsuplem3  47241  fsupdm  47270  finfdm  47274  cfsetsnfsetf  47506  fcores  47515  afvres  47620  afv2res  47687  fundcmpsurinjimaid  47871  iccpartigtl  47883  sprsymrelf  47955  prproropf1olem2  47964  uhgrimedgi  48366  isuspgrim0lem  48369  isuspgrimlem  48371  ushggricedg  48403  grimedg  48411  usgrgrtrirex  48426  isubgr3stgrlem7  48448  uspgrlimlem4  48467  grlimprclnbgr  48472  gpgiedgdmellem  48522  gpg3kgrtriex  48565  funcringcsetcALTV2lem3  48768  funcringcsetclem3ALTV  48791  lindslinindsimp2lem5  48938  rrxsphere  49224  line2  49228  iooii  49393  icccldii  49394  iscnrm3rlem3  49417  eloppf2  49609  oppcup  49682  natoppf  49704  zeroo2  49709  oppfdiag1  49889  oppfdiag  49891  2arwcat  50075  incat  50076  lmddu  50142  onsetreclem3  50182  amgmwlem  50277