Theorem eleqtrrdi 2848

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 2847	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 2709

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

This theorem is referenced by:  3eltr4g  2854  brelrng  5891  elabrex  7191  elabrexg  7192  fliftel1  7259  ovidig  7503  unielxp  7974  tfrlem11  8321  rdglim  8359  seqomlem4  8386  2oconcl  8432  ecopqsi  8711  erov  8755  eroprf  8756  sbthlem2  9020  dffi3  9338  ixpiunwdom  9499  cantnfcl  9582  r1lim  9690  rankwflemb  9711  pwwf  9725  unwf  9728  rankwflem  9733  uniwf  9737  rankpwi  9741  rankr1g  9750  r1pw  9763  r1rankid  9777  rankuni  9781  djulcl  9828  djurcl  9829  inlresf  9832  inrresf  9834  djuun  9844  cardlim  9890  infxpenlem  9929  alephfp  10024  cfsmolem  10186  alephsing  10192  hsmexlem4  10345  axdc3lem2  10367  numth3  10386  iunfo  10455  konigthlem  10485  iunctb  10491  canthwelem  10567  canthwe  10568  r1limwun  10653  inar1  10692  inatsk  10695  gruina  10735  grur1  10737  tskmval  10756  tskmcl  10758  pinq  10844  dmrecnq  10885  addclsr  11000  mulclsr  11001  axaddf  11062  axmulf  11063  peano2nn  12180  uztrn2  12801  eluz2nn  12832  peano2uzs  12846  uzsupss  12884  uzsup  13816  uzrdgfni  13914  uzrdgsuci  13916  fsuppmapnn0fiub  13947  seqf  13979  ser0  14010  bcm1k  14271  bcp1nk  14273  bcpasc  14277  hashprdifel  14354  fz1isolem  14417  pr2pwpr  14435  tpf  14455  ccats1val2  14584  rexuzre  15309  limsupgre  15437  climconst  15499  rlimclim1  15501  climrlim2  15503  clim2ser  15611  clim2ser2  15612  iserex  15613  isermulc2  15614  iserle  15616  isercolllem3  15623  isercoll2  15625  climsup  15626  iseraltlem2  15639  iseraltlem3  15640  zsum  15674  isumclim3  15715  isumadd  15723  fsump1i  15725  iserabs  15772  cvgcmp  15773  cvgcmpub  15774  cvgcmpce  15775  abscvgcvg  15776  isumshft  15798  isumsplit  15799  isum1p  15800  isumrpcl  15802  isumsup2  15805  climcndslem1  15808  cvgrat  15842  clim2prod  15847  clim2div  15848  prodf1  15850  ntrivcvgn0  15857  ntrivcvgtail  15859  fprodntriv  15901  fprodabs  15933  fprodeq0  15934  iprodclim3  15959  iprodmul  15962  ef0lem  16037  fprodefsum  16054  rpnnen2lem3  16177  dvdsflip  16280  fzo0dvdseq  16286  bitsinv1  16405  smupval  16451  smueqlem  16453  seq1st  16534  algr0  16535  prmind2  16648  crth  16742  eulerthlem2  16746  prmdiv  16749  pockthlem  16870  pockthg  16871  unbenlem  16873  prmunb  16879  prmgaplem7  17022  strfv2d  17165  imasvscaval  17496  oppccatid  17679  oppccatf  17688  epii  17704  fthepi  17891  funcestrcsetclem3  18102  funcsetcestrclem3  18116  yon12  18225  yon2  18226  yonedalem4c  18237  yonedalem22  18238  yonedalem3b  18239  yonedainv  18241  acsmapd  18514  chnub  18582  chnccats1  18585  chnccat  18586  mgm2nsgrplem1  18883  mgm2nsgrplem2  18884  mgm2nsgrplem3  18885  sgrp2nmndlem1  18888  sgrp2rid2  18891  ghmqusker  19256  cntrsubgnsg  19312  symgpssefmnd  19365  pmtrrn  19426  gexcl3  19556  efgi  19688  efgi2  19694  efgs1b  19705  efgredlemg  19711  efgredlemd  19713  frgpnabllem1  19842  cycsubgcyg  19870  gsumzaddlem  19890  dprdwd  19982  dprd2da  20013  rhmopp  20480  lsppratlem3  21142  lsppratlem4  21143  lbsextlem2  21152  lidl0ALT  21221  lidl1ALT  21224  2idl0  21253  2idl1  21254  domnchr  21525  znf1o  21544  mplsubrglem  21995  mpfconst  22100  mpfproj  22101  mpfind  22106  mhpmulcl  22128  pf1const  22324  pf1id  22325  mpfpf1  22329  pf1mpf  22330  madetsumid  22439  slesolex  22660  pmatcoe1fsupp  22679  mat2pmatbas0  22705  pmatcollpw  22759  pm2mpf1  22777  isclo  23065  indiscld  23069  restntr  23160  ordtbaslem  23166  ordtbas2  23169  lmconst  23239  lmss  23276  conncompid  23409  2ndcomap  23436  locfincmp  23504  comppfsc  23510  xkouni  23577  txcls  23582  ptclsg  23593  uptx  23603  txindis  23612  tx1stc  23628  cnmpt1res  23654  tgqtop  23690  uffix  23899  cnpflf2  23978  ptcmplem2  24031  ptcmplem4  24033  tgpconncomp  24091  tsmsfbas  24106  fmucnd  24269  prdsxmetlem  24346  imasdsf1olem  24351  prdsbl  24469  blcvx  24776  xrsmopn  24791  xrge0tsms  24813  metdcn2  24818  expcncf  24906  cnmpopc  24908  icchmeo  24921  iccpnfhmeo  24925  cnheibor  24935  evth  24939  evth2  24940  lebnumlem2  24942  lebnumii  24946  reparphti  24977  cfilfcls  25254  minveclem2  25406  minveclem3  25409  minveclem4  25412  ovoliunlem1  25482  ovolicc1  25496  iundisj  25528  volsup  25536  uniioombllem3  25565  vitalilem2  25589  vitalilem3  25590  mbfsup  25644  mbfinf  25645  mbflimsup  25646  itg2monolem1  25730  limcflflem  25860  limccnp  25871  limccnp2  25872  dvidlem  25895  dvn2bss  25910  cpnres  25917  dvcobr  25926  dvrec  25935  c1liplem1  25976  dvcnvrelem2  25998  dvfsumrlimf  26005  dvfsumlem1  26006  dvfsumlem2  26007  dvfsumlem3  26008  dvfsumlem4  26009  dvfsumrlim  26011  dvfsum2  26014  coeeulem  26202  coeid3  26218  plycn  26239  dvntaylp  26351  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulm2  26366  ulmshftlem  26370  ulmshft  26371  ulm0  26372  ulmcn  26380  ulmdvlem3  26383  ulmdv  26384  mtest  26385  mtestbdd  26386  dvradcnv  26402  psercn2  26404  psercn  26407  pserdv  26410  abelth  26422  efif1olem2  26523  efif1olem4  26525  efifo  26527  eff1olem  26528  logcn  26627  dvloglem  26628  cxpcn3  26728  resqrtcn  26729  sqrtcn  26730  logbleb  26763  logblt  26764  asinneg  26866  atanlogsub  26896  atanbnd  26906  ressatans  26914  leibpilem2  26921  xrlimcnp  26948  efrlim  26949  efrlimOLD  26950  scvxcvx  26966  ppiub  27184  chtub  27192  logexprlim  27205  lgseisenlem1  27355  rplogsumlem1  27464  rplogsumlem2  27465  dchrisumlem2  27470  dchrisum0flb  27490  logdivbnd  27536  pntlem3  27589  dfnns2  28381  tgcgr4  28616  ltgov  28682  f1otrg  28956  eengtrkg  29072  iedgedg  29136  ushgredgedgloop  29317  subgruhgredgd  29370  uvtxupgrres  29494  umgr2v2evd2  29614  edginwlk  29721  wlk1walk  29725  crctcshwlkn0lem6  29901  wlkiswwlks1  29953  minvecolem1  30963  minvecolem2  30964  minvecolem4  30969  htthlem  31006  5oalem2  31744  3oalem2  31752  iundisjf  32677  fmptco1f1o  32724  xppreima  32736  xppreima2  32742  dfcnv2  32766  ccatws1f1o  33029  gsumhashmul  33146  xrge0tsmsd  33152  gsumwrd2dccatlem  33156  odpmco  33165  pmtrcnelor  33170  fzo0pmtrlast  33171  wrdpmtrlast  33172  pmtrto1cl  33178  psgnfzto1stlem  33179  fzto1stfv1  33180  fzto1st  33182  fzto1stinvn  33183  psgnfzto1st  33184  tocycf  33196  cycpmco2lem7  33211  cycpmco2  33212  cycpmrn  33222  cyc3evpm  33229  cyc3genpmlem  33230  cycpmgcl  33232  cyc3conja  33236  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem3  33323  elrgspnlem4  33324  elrgspnsubrunlem1  33326  nsgmgc  33490  nsgqusf1olem1  33491  nsgqusf1olem2  33492  rhmpreimaprmidl  33529  ssdifidllem  33534  ssdifidl  33535  ssmxidllem  33551  drngmxidlr  33556  opprqus1r  33570  qsdrngilem  33572  qsdrngi  33573  rsprprmprmidlb  33601  rprmirredb  33610  1arithufdlem1  33622  1arithufdlem2  33623  1arithufdlem3  33624  1arithufdlem4  33625  fply1  33636  ply1degltel  33672  ply1degleel  33673  ply1degltlss  33674  mplmulmvr  33701  psrmon  33711  psrmonprod  33714  esplylem  33728  esplyfv1  33731  esplysply  33733  esplyind  33737  ply1degltdimlem  33785  ply1degltdim  33786  algextdeglem4  33883  algextdeglem6  33885  algextdeglem7  33886  algextdeglem8  33887  nn0constr  33924  smatlem  33960  smatcl  33965  zartopn  34038  zarmxt1  34043  tpr2rico  34075  xrmulc1cn  34093  xrge0mulc1cn  34104  esumpfinvallem  34237  ldgenpisyslem1  34326  dynkin  34330  brfae  34411  sxbrsigalem3  34435  dya2icoseg2  34441  omsmeas  34486  sibfof  34503  sseqmw  34554  sseqf  34555  sseqp1  34558  fiblem  34561  fibp1  34564  probfinmeasbALTV  34592  repr0  34774  reprpmtf1o  34789  hgt750lemg  34817  bnj1379  34991  srcmpltd  35241  fineqvnttrclselem3  35286  subfacp1lem5  35385  subfacp1lem6  35386  cvxpconn  35443  cvxsconn  35444  cvmliftlem6  35491  cvmliftlem8  35493  cvmliftlem10  35495  cvmlift2lem6  35509  cvmlift2lem11  35514  cvmlift2lem12  35515  2goelgoanfmla1  35625  prv1n  35632  msubff  35731  msubco  35732  elmsta  35749  msubff1  35757  mvhf  35759  msubvrs  35761  iprodefisumlem  35941  filnetlem3  36581  ttcid  36693  ttcwf  36725  knoppcnlem10  36781  knoppcnlem11  36782  icoreunrn  37692  icoreelrn  37694  ralssiun  37740  poimirlem3  37961  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem30  37988  dvasin  38042  cover2  38053  upixp  38067  sdclem1  38081  fdc  38083  caushft  38099  ismtyres  38146  rrncmslem  38170  isfld2  38343  presuc  38836  osumcllem10N  40428  pexmidlem7N  40439  dihglblem2N  41757  lcfrvalsnN  42004  lcfrlem5  42009  lcfrlem6  42010  lcfrlem27  42032  lcfrlem37  42042  aks6d1c1p4  42567  aks6d1c1p7  42569  aks6d1c1p8  42571  evl1gprodd  42573  aks6d1c2lem4  42583  aks6d1c5lem3  42593  aks6d1c6lem2  42627  prjspvs  43060  0prjspnrel  43077  monotuz  43390  expdiophlem1  43470  kelac2  43514  naddwordnexlem4  43850  grurankcld  44681  dvgrat  44760  nzss  44765  uzmptshftfval  44794  binomcxplemnotnn0  44804  orbitinit  45404  orbitcl  45405  permaxinf2lem  45460  refsumcn  45482  rfcnpre2  45483  rfcnpre3  45485  rfcnpre4  45486  disjf1o  45642  unirnmap  45658  unirnmapsn  45664  ssmapsn  45666  mptssid  45691  allbutfi  45843  eluzd  45858  uzidd2  45865  ressiocsup  46005  ressioosup  46006  ressiooinf  46008  fsumsermpt  46030  climexp  46056  climinf  46057  climsuse  46059  sumnnodd  46081  limsupresico  46149  limsupubuzlem  46161  limsupresxr  46215  liminfresxr  46216  liminfresico  46220  limsup10exlem  46221  cnrefiisplem  46278  cncfiooicclem1  46342  dvsinax  46362  itgsinexplem1  46403  fvvolioof  46438  fvvolicof  46440  stoweidlem14  46463  stoweidlem16  46465  stoweidlem31  46480  stoweidlem34  46483  stoweidlem36  46485  stoweidlem43  46492  stoweidlem46  46495  stoweidlem47  46496  stoweidlem52  46501  stoweidlem55  46504  stoweidlem57  46506  dirkercncf  46556  fourierdlem20  46576  fourierdlem42  46598  fourierdlem48  46603  fourierdlem49  46604  fourierdlem51  46606  fourierdlem54  46609  fourierdlem62  46617  fourierdlem71  46626  fourierdlem80  46635  fourierdlem114  46669  fouriersw  46680  ioorrnopnlem  46753  ioorrnopnxrlem  46755  salexct3  46791  salgencntex  46792  salgensscntex  46793  subsalsal  46808  sge0fodjrnlem  46865  sge0isum  46876  sge0seq  46895  sge0reuz  46896  sge0reuzb  46897  meadjiunlem  46914  meaiininclem  46935  carageniuncllem1  46970  caratheodorylem1  46975  hoiprodp1  47037  hoidmv1lelem1  47040  hoidmv1lelem2  47041  hoidmv1le  47043  hoidmvlelem1  47044  hoidmvlelem2  47045  hoidmvlelem3  47046  voncmpl  47070  hoiqssbl  47074  smflimlem2  47221  smfsuplem1  47260  smfsuplem3  47262  fsupdm  47291  finfdm  47295  cfsetsnfsetf  47521  fcores  47530  afvres  47635  afv2res  47702  fundcmpsurinjimaid  47886  iccpartigtl  47898  sprsymrelf  47970  prproropf1olem2  47979  uhgrimedgi  48381  isuspgrim0lem  48384  isuspgrimlem  48386  ushggricedg  48418  grimedg  48426  usgrgrtrirex  48441  isubgr3stgrlem7  48463  uspgrlimlem4  48482  grlimprclnbgr  48487  gpgiedgdmellem  48537  gpg3kgrtriex  48580  funcringcsetcALTV2lem3  48783  funcringcsetclem3ALTV  48806  lindslinindsimp2lem5  48953  rrxsphere  49239  line2  49243  iooii  49408  icccldii  49409  iscnrm3rlem3  49432  eloppf2  49624  oppcup  49697  natoppf  49719  zeroo2  49724  oppfdiag1  49904  oppfdiag  49906  2arwcat  50090  incat  50091  lmddu  50157  onsetreclem3  50197  amgmwlem  50292