Theorem eleqtrrdi 2901

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  3eltr4g  2907  brelrng  5775  elabrex  6980  fliftel1  7042  ovidig  7271  unielxp  7709  tfrlem11  8007  rdglim  8045  seqomlem4  8072  2oconcl  8111  ecopqsi  8337  erov  8377  eroprf  8378  sbthlem2  8612  dffi3  8879  ixpiunwdom  9038  cantnfcl  9114  r1lim  9185  rankwflemb  9206  pwwf  9220  unwf  9223  rankwflem  9228  uniwf  9232  rankpwi  9236  rankr1g  9245  r1pw  9258  r1rankid  9272  rankuni  9276  djulcl  9323  djurcl  9324  inlresf  9327  inrresf  9329  djuun  9339  cardlim  9385  infxpenlem  9424  alephfp  9519  cfsmolem  9681  alephsing  9687  hsmexlem4  9840  axdc3lem2  9862  numth3  9881  iunfo  9950  konigthlem  9979  iunctb  9985  canthwelem  10061  canthwe  10062  r1limwun  10147  inar1  10186  inatsk  10189  gruina  10229  grur1  10231  tskmval  10250  tskmcl  10252  pinq  10338  dmrecnq  10379  addclsr  10494  mulclsr  10495  axaddf  10556  axmulf  10557  peano2nn  11637  uztrn2  12250  eluz2nn  12272  peano2uzs  12290  uzsupss  12328  uzsup  13226  uzrdgfni  13321  uzrdgsuci  13323  fsuppmapnn0fiub  13354  seqf  13387  ser0  13418  bcm1k  13671  bcp1nk  13673  bcpasc  13677  hashprdifel  13755  fz1isolem  13815  pr2pwpr  13833  ccats1val2  13974  rexuzre  14704  limsupgre  14830  climconst  14892  rlimclim1  14894  climrlim2  14896  clim2ser  15003  clim2ser2  15004  iserex  15005  isermulc2  15006  iserle  15008  isercolllem3  15015  isercoll2  15017  climsup  15018  iseraltlem2  15031  iseraltlem3  15032  zsum  15067  isumclim3  15106  isumadd  15114  fsump1i  15116  iserabs  15162  cvgcmp  15163  cvgcmpub  15164  cvgcmpce  15165  abscvgcvg  15166  isumshft  15186  isumsplit  15187  isum1p  15188  isumrpcl  15190  isumsup2  15193  climcndslem1  15196  cvgrat  15231  clim2prod  15236  clim2div  15237  prodf1  15239  ntrivcvgn0  15246  ntrivcvgtail  15248  fprodntriv  15288  fprodabs  15320  fprodeq0  15321  iprodclim3  15346  iprodmul  15349  ef0lem  15424  fprodefsum  15440  rpnnen2lem3  15561  dvdsflip  15659  fzo0dvdseq  15665  bitsinv1  15781  smupval  15827  smueqlem  15829  seq1st  15905  algr0  15906  prmind2  16019  crth  16105  eulerthlem2  16109  prmdiv  16112  pockthlem  16231  pockthg  16232  unbenlem  16234  prmunb  16240  prmgaplem7  16383  strfv2d  16521  imasvscaval  16803  oppccatid  16981  epii  17005  fthepi  17190  funcestrcsetclem3  17384  funcsetcestrclem3  17398  yon12  17507  yon2  17508  yonedalem4c  17519  yonedalem22  17520  yonedalem3b  17521  yonedainv  17523  acsmapd  17780  mgm2nsgrplem1  18075  mgm2nsgrplem2  18076  mgm2nsgrplem3  18077  sgrp2nmndlem1  18080  sgrp2rid2  18083  cntrsubgnsg  18463  symgpssefmnd  18516  pmtrrn  18577  gexcl3  18704  efgi  18837  efgi2  18843  efgs1b  18854  efgredlemg  18860  efgredlemd  18862  frgpnabllem1  18986  cycsubgcyg  19014  gsumzaddlem  19034  dprdwd  19126  dprd2da  19157  lsppratlem3  19914  lsppratlem4  19915  lbsextlem2  19924  lidl0  19985  lidl1  19986  domnchr  20224  znf1o  20243  mplsubrglem  20677  mpfconst  20773  mpfproj  20774  mpfind  20779  pf1const  20970  pf1id  20971  mpfpf1  20975  pf1mpf  20976  madetsumid  21066  slesolex  21287  pmatcoe1fsupp  21306  mat2pmatbas0  21332  pmatcollpw  21386  pm2mpf1  21404  isclo  21692  indiscld  21696  restntr  21787  ordtbaslem  21793  ordtbas2  21796  lmconst  21866  lmss  21903  conncompid  22036  2ndcomap  22063  locfincmp  22131  comppfsc  22137  xkouni  22204  txcls  22209  ptclsg  22220  uptx  22230  txindis  22239  tx1stc  22255  cnmpt1res  22281  tgqtop  22317  uffix  22526  cnpflf2  22605  ptcmplem2  22658  ptcmplem4  22660  tgpconncomp  22718  tsmsfbas  22733  fmucnd  22898  prdsxmetlem  22975  imasdsf1olem  22980  prdsbl  23098  blcvx  23403  xrsmopn  23417  xrge0tsms  23439  metdcn2  23444  expcncf  23531  cnmpopc  23533  icchmeo  23546  iccpnfhmeo  23550  cnheibor  23560  evth  23564  evth2  23565  lebnumlem2  23567  lebnumii  23571  reparphti  23602  cfilfcls  23878  minveclem2  24030  minveclem3  24033  minveclem4  24036  ovoliunlem1  24106  ovolicc1  24120  iundisj  24152  volsup  24160  uniioombllem3  24189  vitalilem2  24213  vitalilem3  24214  mbfsup  24268  mbfinf  24269  mbflimsup  24270  itg2monolem1  24354  limcflflem  24483  limccnp  24494  limccnp2  24495  dvidlem  24518  dvn2bss  24533  cpnres  24540  dvcobr  24549  dvrec  24558  c1liplem1  24599  dvcnvrelem2  24621  dvfsumrlimf  24628  dvfsumlem1  24629  dvfsumlem2  24630  dvfsumlem3  24631  dvfsumlem4  24632  dvfsumrlim  24634  dvfsum2  24637  coeeulem  24821  coeid3  24837  plycn  24858  dvntaylp  24966  taylthlem1  24968  taylthlem2  24969  ulm2  24980  ulmshftlem  24984  ulmshft  24985  ulm0  24986  ulmcn  24994  ulmdvlem3  24997  ulmdv  24998  mtest  24999  mtestbdd  25000  dvradcnv  25016  psercn2  25018  psercn  25021  pserdv  25024  abelth  25036  efif1olem2  25135  efif1olem4  25137  efifo  25139  eff1olem  25140  logcn  25238  dvloglem  25239  cxpcn3  25337  resqrtcn  25338  sqrtcn  25339  logbleb  25369  logblt  25370  asinneg  25472  atanlogsub  25502  atanbnd  25512  ressatans  25520  leibpilem2  25527  xrlimcnp  25554  efrlim  25555  scvxcvx  25571  ppiub  25788  chtub  25796  logexprlim  25809  lgseisenlem1  25959  rplogsumlem1  26068  rplogsumlem2  26069  dchrisumlem2  26074  dchrisum0flb  26094  logdivbnd  26140  pntlem3  26193  tgcgr4  26325  ltgov  26391  f1otrg  26665  eengtrkg  26780  iedgedg  26843  ushgredgedgloop  27021  subgruhgredgd  27074  uvtxupgrres  27198  umgr2v2evd2  27317  edginwlk  27424  wlk1walk  27428  crctcshwlkn0lem6  27601  wlkiswwlks1  27653  minvecolem1  28657  minvecolem2  28658  minvecolem4  28663  htthlem  28700  5oalem2  29438  3oalem2  29446  iundisjf  30352  fmptco1f1o  30392  xppreima  30408  xppreima2  30413  dfcnv2  30439  gsumhashmul  30741  xrge0tsmsd  30742  odpmco  30780  pmtrcnelor  30785  pmtrto1cl  30791  psgnfzto1stlem  30792  fzto1stfv1  30793  fzto1st  30795  fzto1stinvn  30796  psgnfzto1st  30797  tocycf  30809  cycpmco2lem7  30824  cycpmco2  30825  cycpmrn  30835  cyc3evpm  30842  cyc3genpmlem  30843  cycpmgcl  30845  cyc3conja  30849  rhmopp  30943  fply1  30982  rhmpreimaprmidl  31035  ssmxidllem  31049  smatlem  31150  smatcl  31155  zartopn  31228  zarmxt1  31233  tpr2rico  31265  xrmulc1cn  31283  xrge0mulc1cn  31294  esumpfinvallem  31443  ldgenpisyslem1  31532  dynkin  31536  brfae  31617  sxbrsigalem3  31640  dya2icoseg2  31646  omsmeas  31691  sibfof  31708  sseqmw  31759  sseqf  31760  sseqp1  31763  fiblem  31766  fibp1  31769  probfinmeasbALTV  31797  repr0  31992  reprpmtf1o  32007  hgt750lemg  32035  bnj1379  32212  srcmpltd  32456  subfacp1lem5  32544  subfacp1lem6  32545  cvxpconn  32602  cvxsconn  32603  cvmliftlem6  32650  cvmliftlem8  32652  cvmliftlem10  32654  cvmlift2lem6  32668  cvmlift2lem11  32673  cvmlift2lem12  32674  2goelgoanfmla1  32784  prv1n  32791  msubff  32890  msubco  32891  elmsta  32908  msubff1  32916  mvhf  32918  msubvrs  32920  iprodefisumlem  33085  filnetlem3  33841  knoppcnlem10  33954  knoppcnlem11  33955  icoreunrn  34776  icoreelrn  34778  ralssiun  34824  poimirlem3  35060  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem30  35087  dvasin  35141  cover2  35152  upixp  35167  sdclem1  35181  fdc  35183  caushft  35199  ismtyres  35246  rrncmslem  35270  isfld2  35443  osumcllem10N  37261  pexmidlem7N  37272  dihglblem2N  38590  lcfrvalsnN  38837  lcfrlem5  38842  lcfrlem6  38843  lcfrlem27  38865  lcfrlem37  38875  prjspvs  39604  0prjspnrel  39613  monotuz  39882  expdiophlem1  39962  kelac2  40009  grurankcld  40941  dvgrat  41016  nzss  41021  uzmptshftfval  41050  binomcxplemnotnn0  41060  refsumcn  41659  rfcnpre2  41660  rfcnpre3  41662  rfcnpre4  41663  elabrexg  41675  disjf1o  41818  unirnmap  41837  unirnmapsn  41843  ssmapsn  41845  mptssid  41877  allbutfi  42029  eluzd  42046  uzidd2  42053  ressiocsup  42191  ressioosup  42192  ressiooinf  42194  fsumsermpt  42221  climexp  42247  climinf  42248  climsuse  42250  sumnnodd  42272  limsupresico  42342  limsupubuzlem  42354  limsupresxr  42408  liminfresxr  42409  liminfresico  42413  limsup10exlem  42414  cnrefiisplem  42471  cncfiooicclem1  42535  dvsinax  42555  itgsinexplem1  42596  fvvolioof  42631  fvvolicof  42633  stoweidlem14  42656  stoweidlem16  42658  stoweidlem31  42673  stoweidlem34  42676  stoweidlem36  42678  stoweidlem43  42685  stoweidlem46  42688  stoweidlem47  42689  stoweidlem52  42694  stoweidlem55  42697  stoweidlem57  42699  dirkercncf  42749  fourierdlem20  42769  fourierdlem42  42791  fourierdlem48  42796  fourierdlem49  42797  fourierdlem51  42799  fourierdlem54  42802  fourierdlem62  42810  fourierdlem71  42819  fourierdlem80  42828  fourierdlem114  42862  fouriersw  42873  ioorrnopnlem  42946  ioorrnopnxrlem  42948  salexct3  42982  salgencntex  42983  salgensscntex  42984  subsalsal  42999  sge0fodjrnlem  43055  sge0isum  43066  sge0seq  43085  sge0reuz  43086  sge0reuzb  43087  meadjiunlem  43104  meaiininclem  43125  carageniuncllem1  43160  caratheodorylem1  43165  hoiprodp1  43227  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  voncmpl  43260  hoiqssbl  43264  smflimlem2  43405  smfsuplem1  43442  smfsuplem3  43444  afvres  43728  afv2res  43795  fundcmpsurinjimaid  43928  iccpartigtl  43940  sprsymrelf  44012  prproropf1olem2  44021  ushrisomgr  44359  funcringcsetcALTV2lem3  44662  funcringcsetclem3ALTV  44685  lindslinindsimp2lem5  44871  rrxsphere  45162  line2  45166  onsetreclem3  45236  amgmwlem  45330