Theorem eleqtrrdi 2840

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 2839	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  3eltr4g  2846  brelrng  5908  elabrex  7219  elabrexg  7220  fliftel1  7288  ovidig  7534  unielxp  8009  tfrlem11  8359  rdglim  8397  seqomlem4  8424  2oconcl  8470  ecopqsi  8747  erov  8790  eroprf  8791  sbthlem2  9058  dffi3  9389  ixpiunwdom  9550  cantnfcl  9627  r1lim  9732  rankwflemb  9753  pwwf  9767  unwf  9770  rankwflem  9775  uniwf  9779  rankpwi  9783  rankr1g  9792  r1pw  9805  r1rankid  9819  rankuni  9823  djulcl  9870  djurcl  9871  inlresf  9874  inrresf  9876  djuun  9886  cardlim  9932  infxpenlem  9973  alephfp  10068  cfsmolem  10230  alephsing  10236  hsmexlem4  10389  axdc3lem2  10411  numth3  10430  iunfo  10499  konigthlem  10528  iunctb  10534  canthwelem  10610  canthwe  10611  r1limwun  10696  inar1  10735  inatsk  10738  gruina  10778  grur1  10780  tskmval  10799  tskmcl  10801  pinq  10887  dmrecnq  10928  addclsr  11043  mulclsr  11044  axaddf  11105  axmulf  11106  peano2nn  12205  uztrn2  12819  eluz2nn  12854  peano2uzs  12868  uzsupss  12906  uzsup  13832  uzrdgfni  13930  uzrdgsuci  13932  fsuppmapnn0fiub  13963  seqf  13995  ser0  14026  bcm1k  14287  bcp1nk  14289  bcpasc  14293  hashprdifel  14370  fz1isolem  14433  pr2pwpr  14451  tpf  14471  ccats1val2  14599  rexuzre  15326  limsupgre  15454  climconst  15516  rlimclim1  15518  climrlim2  15520  clim2ser  15628  clim2ser2  15629  iserex  15630  isermulc2  15631  iserle  15633  isercolllem3  15640  isercoll2  15642  climsup  15643  iseraltlem2  15656  iseraltlem3  15657  zsum  15691  isumclim3  15732  isumadd  15740  fsump1i  15742  iserabs  15788  cvgcmp  15789  cvgcmpub  15790  cvgcmpce  15791  abscvgcvg  15792  isumshft  15812  isumsplit  15813  isum1p  15814  isumrpcl  15816  isumsup2  15819  climcndslem1  15822  cvgrat  15856  clim2prod  15861  clim2div  15862  prodf1  15864  ntrivcvgn0  15871  ntrivcvgtail  15873  fprodntriv  15915  fprodabs  15947  fprodeq0  15948  iprodclim3  15973  iprodmul  15976  ef0lem  16051  fprodefsum  16068  rpnnen2lem3  16191  dvdsflip  16294  fzo0dvdseq  16300  bitsinv1  16419  smupval  16465  smueqlem  16467  seq1st  16548  algr0  16549  prmind2  16662  crth  16755  eulerthlem2  16759  prmdiv  16762  pockthlem  16883  pockthg  16884  unbenlem  16886  prmunb  16892  prmgaplem7  17035  strfv2d  17178  imasvscaval  17508  oppccatid  17687  oppccatf  17696  epii  17712  fthepi  17899  funcestrcsetclem3  18110  funcsetcestrclem3  18124  yon12  18233  yon2  18234  yonedalem4c  18245  yonedalem22  18246  yonedalem3b  18247  yonedainv  18249  acsmapd  18520  mgm2nsgrplem1  18852  mgm2nsgrplem2  18853  mgm2nsgrplem3  18854  sgrp2nmndlem1  18857  sgrp2rid2  18860  ghmqusker  19226  cntrsubgnsg  19282  symgpssefmnd  19333  pmtrrn  19394  gexcl3  19524  efgi  19656  efgi2  19662  efgs1b  19673  efgredlemg  19679  efgredlemd  19681  frgpnabllem1  19810  cycsubgcyg  19838  gsumzaddlem  19858  dprdwd  19950  dprd2da  19981  rhmopp  20425  lsppratlem3  21066  lsppratlem4  21067  lbsextlem2  21076  lidl0ALT  21145  lidl1ALT  21148  2idl0  21177  2idl1  21178  domnchr  21449  znf1o  21468  mplsubrglem  21920  mpfconst  22015  mpfproj  22016  mpfind  22021  mhpmulcl  22043  pf1const  22240  pf1id  22241  mpfpf1  22245  pf1mpf  22246  madetsumid  22355  slesolex  22576  pmatcoe1fsupp  22595  mat2pmatbas0  22621  pmatcollpw  22675  pm2mpf1  22693  isclo  22981  indiscld  22985  restntr  23076  ordtbaslem  23082  ordtbas2  23085  lmconst  23155  lmss  23192  conncompid  23325  2ndcomap  23352  locfincmp  23420  comppfsc  23426  xkouni  23493  txcls  23498  ptclsg  23509  uptx  23519  txindis  23528  tx1stc  23544  cnmpt1res  23570  tgqtop  23606  uffix  23815  cnpflf2  23894  ptcmplem2  23947  ptcmplem4  23949  tgpconncomp  24007  tsmsfbas  24022  fmucnd  24186  prdsxmetlem  24263  imasdsf1olem  24268  prdsbl  24386  blcvx  24693  xrsmopn  24708  xrge0tsms  24730  metdcn2  24735  expcncf  24827  cnmpopc  24829  icchmeo  24845  icchmeoOLD  24846  iccpnfhmeo  24850  cnheibor  24861  evth  24865  evth2  24866  lebnumlem2  24868  lebnumii  24872  reparphti  24903  reparphtiOLD  24904  cfilfcls  25181  minveclem2  25333  minveclem3  25336  minveclem4  25339  ovoliunlem1  25410  ovolicc1  25424  iundisj  25456  volsup  25464  uniioombllem3  25493  vitalilem2  25517  vitalilem3  25518  mbfsup  25572  mbfinf  25573  mbflimsup  25574  itg2monolem1  25658  limcflflem  25788  limccnp  25799  limccnp2  25800  dvidlem  25823  dvn2bss  25839  cpnres  25846  dvcobr  25856  dvcobrOLD  25857  dvrec  25866  c1liplem1  25908  dvcnvrelem2  25930  dvfsumrlimf  25938  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsumrlim  25945  dvfsum2  25948  coeeulem  26136  coeid3  26152  plycn  26173  plycnOLD  26174  dvntaylp  26286  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulm2  26301  ulmshftlem  26305  ulmshft  26306  ulm0  26307  ulmcn  26315  ulmdvlem3  26318  ulmdv  26319  mtest  26320  mtestbdd  26321  dvradcnv  26337  psercn2  26339  psercn2OLD  26340  psercn  26343  pserdv  26346  abelth  26358  efif1olem2  26459  efif1olem4  26461  efifo  26463  eff1olem  26464  logcn  26563  dvloglem  26564  cxpcn3  26665  resqrtcn  26666  sqrtcn  26667  logbleb  26700  logblt  26701  asinneg  26803  atanlogsub  26833  atanbnd  26843  ressatans  26851  leibpilem2  26858  xrlimcnp  26885  efrlim  26886  efrlimOLD  26887  scvxcvx  26903  ppiub  27122  chtub  27130  logexprlim  27143  lgseisenlem1  27293  rplogsumlem1  27402  rplogsumlem2  27403  dchrisumlem2  27408  dchrisum0flb  27428  logdivbnd  27474  pntlem3  27527  dfnns2  28268  tgcgr4  28465  ltgov  28531  f1otrg  28805  eengtrkg  28920  iedgedg  28984  ushgredgedgloop  29165  subgruhgredgd  29218  uvtxupgrres  29342  umgr2v2evd2  29462  edginwlk  29570  wlk1walk  29574  crctcshwlkn0lem6  29752  wlkiswwlks1  29804  minvecolem1  30810  minvecolem2  30811  minvecolem4  30816  htthlem  30853  5oalem2  31591  3oalem2  31599  iundisjf  32525  fmptco1f1o  32564  xppreima  32576  xppreima2  32582  dfcnv2  32607  ccatws1f1o  32880  chnub  32945  chnccats1  32948  gsumhashmul  33008  xrge0tsmsd  33009  gsumwrd2dccatlem  33013  odpmco  33050  pmtrcnelor  33055  fzo0pmtrlast  33056  wrdpmtrlast  33057  pmtrto1cl  33063  psgnfzto1stlem  33064  fzto1stfv1  33065  fzto1st  33067  fzto1stinvn  33068  psgnfzto1st  33069  tocycf  33081  cycpmco2lem7  33096  cycpmco2  33097  cycpmrn  33107  cyc3evpm  33114  cyc3genpmlem  33115  cycpmgcl  33117  cyc3conja  33121  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspnsubrunlem1  33205  nsgmgc  33390  nsgqusf1olem1  33391  nsgqusf1olem2  33392  rhmpreimaprmidl  33429  ssdifidllem  33434  ssdifidl  33435  ssmxidllem  33451  drngmxidlr  33456  opprqus1r  33470  qsdrngilem  33472  qsdrngi  33473  rsprprmprmidlb  33501  rprmirredb  33510  1arithufdlem1  33522  1arithufdlem2  33523  1arithufdlem3  33524  1arithufdlem4  33525  fply1  33534  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  ply1degltdimlem  33625  ply1degltdim  33626  algextdeglem4  33717  algextdeglem6  33719  algextdeglem7  33720  algextdeglem8  33721  nn0constr  33758  smatlem  33794  smatcl  33799  zartopn  33872  zarmxt1  33877  tpr2rico  33909  xrmulc1cn  33927  xrge0mulc1cn  33938  esumpfinvallem  34071  ldgenpisyslem1  34160  dynkin  34164  brfae  34245  sxbrsigalem3  34270  dya2icoseg2  34276  omsmeas  34321  sibfof  34338  sseqmw  34389  sseqf  34390  sseqp1  34393  fiblem  34396  fibp1  34399  probfinmeasbALTV  34427  repr0  34609  reprpmtf1o  34624  hgt750lemg  34652  bnj1379  34827  srcmpltd  35077  subfacp1lem5  35178  subfacp1lem6  35179  cvxpconn  35236  cvxsconn  35237  cvmliftlem6  35284  cvmliftlem8  35286  cvmliftlem10  35288  cvmlift2lem6  35302  cvmlift2lem11  35307  cvmlift2lem12  35308  2goelgoanfmla1  35418  prv1n  35425  msubff  35524  msubco  35525  elmsta  35542  msubff1  35550  mvhf  35552  msubvrs  35554  iprodefisumlem  35734  filnetlem3  36375  knoppcnlem10  36497  knoppcnlem11  36498  icoreunrn  37354  icoreelrn  37356  ralssiun  37402  poimirlem3  37624  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem30  37651  dvasin  37705  cover2  37716  upixp  37730  sdclem1  37744  fdc  37746  caushft  37762  ismtyres  37809  rrncmslem  37833  isfld2  38006  osumcllem10N  39966  pexmidlem7N  39977  dihglblem2N  41295  lcfrvalsnN  41542  lcfrlem5  41547  lcfrlem6  41548  lcfrlem27  41570  lcfrlem37  41580  aks6d1c1p4  42106  aks6d1c1p7  42108  aks6d1c1p8  42110  evl1gprodd  42112  aks6d1c2lem4  42122  aks6d1c5lem3  42132  aks6d1c6lem2  42166  prjspvs  42605  0prjspnrel  42622  monotuz  42937  expdiophlem1  43017  kelac2  43061  naddwordnexlem4  43397  grurankcld  44229  dvgrat  44308  nzss  44313  uzmptshftfval  44342  binomcxplemnotnn0  44352  orbitinit  44953  orbitcl  44954  permaxinf2lem  45009  refsumcn  45031  rfcnpre2  45032  rfcnpre3  45034  rfcnpre4  45035  disjf1o  45192  unirnmap  45209  unirnmapsn  45215  ssmapsn  45217  mptssid  45242  allbutfi  45396  eluzd  45412  uzidd2  45419  ressiocsup  45559  ressioosup  45560  ressiooinf  45562  fsumsermpt  45584  climexp  45610  climinf  45611  climsuse  45613  sumnnodd  45635  limsupresico  45705  limsupubuzlem  45717  limsupresxr  45771  liminfresxr  45772  liminfresico  45776  limsup10exlem  45777  cnrefiisplem  45834  cncfiooicclem1  45898  dvsinax  45918  itgsinexplem1  45959  fvvolioof  45994  fvvolicof  45996  stoweidlem14  46019  stoweidlem16  46021  stoweidlem31  46036  stoweidlem34  46039  stoweidlem36  46041  stoweidlem43  46048  stoweidlem46  46051  stoweidlem47  46052  stoweidlem52  46057  stoweidlem55  46060  stoweidlem57  46062  dirkercncf  46112  fourierdlem20  46132  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem54  46165  fourierdlem62  46173  fourierdlem71  46182  fourierdlem80  46191  fourierdlem114  46225  fouriersw  46236  ioorrnopnlem  46309  ioorrnopnxrlem  46311  salexct3  46347  salgencntex  46348  salgensscntex  46349  subsalsal  46364  sge0fodjrnlem  46421  sge0isum  46432  sge0seq  46451  sge0reuz  46452  sge0reuzb  46453  meadjiunlem  46470  meaiininclem  46491  carageniuncllem1  46526  caratheodorylem1  46531  hoiprodp1  46593  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  voncmpl  46626  hoiqssbl  46630  smflimlem2  46777  smfsuplem1  46816  smfsuplem3  46818  fsupdm  46847  finfdm  46851  cfsetsnfsetf  47063  fcores  47072  afvres  47177  afv2res  47244  fundcmpsurinjimaid  47416  iccpartigtl  47428  sprsymrelf  47500  prproropf1olem2  47509  uhgrimedgi  47894  isuspgrim0lem  47897  isuspgrimlem  47899  ushggricedg  47931  grimedg  47939  usgrgrtrirex  47953  isubgr3stgrlem7  47975  uspgrlimlem4  47994  gpgiedgdmellem  48041  gpg3kgrtriex  48084  funcringcsetcALTV2lem3  48284  funcringcsetclem3ALTV  48307  lindslinindsimp2lem5  48455  rrxsphere  48741  line2  48745  iooii  48910  icccldii  48911  iscnrm3rlem3  48934  eloppf2  49127  oppcup  49200  natoppf  49222  zeroo2  49227  oppfdiag1  49407  oppfdiag  49409  2arwcat  49593  incat  49594  lmddu  49660  onsetreclem3  49700  amgmwlem  49795