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 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  3eltr4g  2853  brelrng  5890  elabrex  7188  elabrexg  7189  fliftel1  7256  ovidig  7500  unielxp  7971  tfrlem11  8319  rdglim  8357  seqomlem4  8384  2oconcl  8430  ecopqsi  8709  erov  8753  eroprf  8754  sbthlem2  9018  dffi3  9336  ixpiunwdom  9497  cantnfcl  9578  r1lim  9686  rankwflemb  9707  pwwf  9721  unwf  9724  rankwflem  9729  uniwf  9733  rankpwi  9737  rankr1g  9746  r1pw  9759  r1rankid  9773  rankuni  9777  djulcl  9824  djurcl  9825  inlresf  9828  inrresf  9830  djuun  9840  cardlim  9886  infxpenlem  9925  alephfp  10020  cfsmolem  10182  alephsing  10188  hsmexlem4  10341  axdc3lem2  10363  numth3  10382  iunfo  10451  konigthlem  10481  iunctb  10487  canthwelem  10563  canthwe  10564  r1limwun  10649  inar1  10688  inatsk  10691  gruina  10731  grur1  10733  tskmval  10752  tskmcl  10754  pinq  10840  dmrecnq  10881  addclsr  10996  mulclsr  10997  axaddf  11058  axmulf  11059  peano2nn  12159  uztrn2  12772  eluz2nn  12803  peano2uzs  12817  uzsupss  12855  uzsup  13785  uzrdgfni  13883  uzrdgsuci  13885  fsuppmapnn0fiub  13916  seqf  13948  ser0  13979  bcm1k  14240  bcp1nk  14242  bcpasc  14246  hashprdifel  14323  fz1isolem  14386  pr2pwpr  14404  tpf  14424  ccats1val2  14553  rexuzre  15278  limsupgre  15406  climconst  15468  rlimclim1  15470  climrlim2  15472  clim2ser  15580  clim2ser2  15581  iserex  15582  isermulc2  15583  iserle  15585  isercolllem3  15592  isercoll2  15594  climsup  15595  iseraltlem2  15608  iseraltlem3  15609  zsum  15643  isumclim3  15684  isumadd  15692  fsump1i  15694  iserabs  15740  cvgcmp  15741  cvgcmpub  15742  cvgcmpce  15743  abscvgcvg  15744  isumshft  15764  isumsplit  15765  isum1p  15766  isumrpcl  15768  isumsup2  15771  climcndslem1  15774  cvgrat  15808  clim2prod  15813  clim2div  15814  prodf1  15816  ntrivcvgn0  15823  ntrivcvgtail  15825  fprodntriv  15867  fprodabs  15899  fprodeq0  15900  iprodclim3  15925  iprodmul  15928  ef0lem  16003  fprodefsum  16020  rpnnen2lem3  16143  dvdsflip  16246  fzo0dvdseq  16252  bitsinv1  16371  smupval  16417  smueqlem  16419  seq1st  16500  algr0  16501  prmind2  16614  crth  16707  eulerthlem2  16711  prmdiv  16714  pockthlem  16835  pockthg  16836  unbenlem  16838  prmunb  16844  prmgaplem7  16987  strfv2d  17130  imasvscaval  17461  oppccatid  17644  oppccatf  17653  epii  17669  fthepi  17856  funcestrcsetclem3  18067  funcsetcestrclem3  18081  yon12  18190  yon2  18191  yonedalem4c  18202  yonedalem22  18203  yonedalem3b  18204  yonedainv  18206  acsmapd  18479  chnub  18547  chnccats1  18550  chnccat  18551  mgm2nsgrplem1  18845  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  sgrp2nmndlem1  18850  sgrp2rid2  18853  ghmqusker  19218  cntrsubgnsg  19274  symgpssefmnd  19327  pmtrrn  19388  gexcl3  19518  efgi  19650  efgi2  19656  efgs1b  19667  efgredlemg  19673  efgredlemd  19675  frgpnabllem1  19804  cycsubgcyg  19832  gsumzaddlem  19852  dprdwd  19944  dprd2da  19975  rhmopp  20444  lsppratlem3  21106  lsppratlem4  21107  lbsextlem2  21116  lidl0ALT  21185  lidl1ALT  21188  2idl0  21217  2idl1  21218  domnchr  21489  znf1o  21508  mplsubrglem  21961  mpfconst  22066  mpfproj  22067  mpfind  22072  mhpmulcl  22094  pf1const  22292  pf1id  22293  mpfpf1  22297  pf1mpf  22298  madetsumid  22407  slesolex  22628  pmatcoe1fsupp  22647  mat2pmatbas0  22673  pmatcollpw  22727  pm2mpf1  22745  isclo  23033  indiscld  23037  restntr  23128  ordtbaslem  23134  ordtbas2  23137  lmconst  23207  lmss  23244  conncompid  23377  2ndcomap  23404  locfincmp  23472  comppfsc  23478  xkouni  23545  txcls  23550  ptclsg  23561  uptx  23571  txindis  23580  tx1stc  23596  cnmpt1res  23622  tgqtop  23658  uffix  23867  cnpflf2  23946  ptcmplem2  23999  ptcmplem4  24001  tgpconncomp  24059  tsmsfbas  24074  fmucnd  24237  prdsxmetlem  24314  imasdsf1olem  24319  prdsbl  24437  blcvx  24744  xrsmopn  24759  xrge0tsms  24781  metdcn2  24786  expcncf  24878  cnmpopc  24880  icchmeo  24896  icchmeoOLD  24897  iccpnfhmeo  24901  cnheibor  24912  evth  24916  evth2  24917  lebnumlem2  24919  lebnumii  24923  reparphti  24954  reparphtiOLD  24955  cfilfcls  25232  minveclem2  25384  minveclem3  25387  minveclem4  25390  ovoliunlem1  25461  ovolicc1  25475  iundisj  25507  volsup  25515  uniioombllem3  25544  vitalilem2  25568  vitalilem3  25569  mbfsup  25623  mbfinf  25624  mbflimsup  25625  itg2monolem1  25709  limcflflem  25839  limccnp  25850  limccnp2  25851  dvidlem  25874  dvn2bss  25890  cpnres  25897  dvcobr  25907  dvcobrOLD  25908  dvrec  25917  c1liplem1  25959  dvcnvrelem2  25981  dvfsumrlimf  25989  dvfsumlem1  25990  dvfsumlem2  25991  dvfsumlem2OLD  25992  dvfsumlem3  25993  dvfsumlem4  25994  dvfsumrlim  25996  dvfsum2  25999  coeeulem  26187  coeid3  26203  plycn  26224  plycnOLD  26225  dvntaylp  26337  taylthlem1  26339  taylthlem2  26340  taylthlem2OLD  26341  ulm2  26352  ulmshftlem  26356  ulmshft  26357  ulm0  26358  ulmcn  26366  ulmdvlem3  26369  ulmdv  26370  mtest  26371  mtestbdd  26372  dvradcnv  26388  psercn2  26390  psercn2OLD  26391  psercn  26394  pserdv  26397  abelth  26409  efif1olem2  26510  efif1olem4  26512  efifo  26514  eff1olem  26515  logcn  26614  dvloglem  26615  cxpcn3  26716  resqrtcn  26717  sqrtcn  26718  logbleb  26751  logblt  26752  asinneg  26854  atanlogsub  26884  atanbnd  26894  ressatans  26902  leibpilem2  26909  xrlimcnp  26936  efrlim  26937  efrlimOLD  26938  scvxcvx  26954  ppiub  27173  chtub  27181  logexprlim  27194  lgseisenlem1  27344  rplogsumlem1  27453  rplogsumlem2  27454  dchrisumlem2  27459  dchrisum0flb  27479  logdivbnd  27525  pntlem3  27578  dfnns2  28370  tgcgr4  28605  ltgov  28671  f1otrg  28945  eengtrkg  29061  iedgedg  29125  ushgredgedgloop  29306  subgruhgredgd  29359  uvtxupgrres  29483  umgr2v2evd2  29603  edginwlk  29710  wlk1walk  29714  crctcshwlkn0lem6  29890  wlkiswwlks1  29942  minvecolem1  30951  minvecolem2  30952  minvecolem4  30957  htthlem  30994  5oalem2  31732  3oalem2  31740  iundisjf  32666  fmptco1f1o  32713  xppreima  32725  xppreima2  32731  dfcnv2  32756  ccatws1f1o  33035  gsumhashmul  33152  xrge0tsmsd  33157  gsumwrd2dccatlem  33161  odpmco  33170  pmtrcnelor  33175  fzo0pmtrlast  33176  wrdpmtrlast  33177  pmtrto1cl  33183  psgnfzto1stlem  33184  fzto1stfv1  33185  fzto1st  33187  fzto1stinvn  33188  psgnfzto1st  33189  tocycf  33201  cycpmco2lem7  33216  cycpmco2  33217  cycpmrn  33227  cyc3evpm  33234  cyc3genpmlem  33235  cycpmgcl  33237  cyc3conja  33241  elrgspnlem1  33326  elrgspnlem2  33327  elrgspnlem3  33328  elrgspnlem4  33329  elrgspnsubrunlem1  33331  nsgmgc  33495  nsgqusf1olem1  33496  nsgqusf1olem2  33497  rhmpreimaprmidl  33534  ssdifidllem  33539  ssdifidl  33540  ssmxidllem  33556  drngmxidlr  33561  opprqus1r  33575  qsdrngilem  33577  qsdrngi  33578  rsprprmprmidlb  33606  rprmirredb  33615  1arithufdlem1  33627  1arithufdlem2  33628  1arithufdlem3  33629  1arithufdlem4  33630  fply1  33641  ply1degltel  33677  ply1degleel  33678  ply1degltlss  33679  mplmulmvr  33706  esplylem  33726  esplyfv1  33729  esplysply  33731  esplyind  33733  ply1degltdimlem  33781  ply1degltdim  33782  algextdeglem4  33879  algextdeglem6  33881  algextdeglem7  33882  algextdeglem8  33883  nn0constr  33920  smatlem  33956  smatcl  33961  zartopn  34034  zarmxt1  34039  tpr2rico  34071  xrmulc1cn  34089  xrge0mulc1cn  34100  esumpfinvallem  34233  ldgenpisyslem1  34322  dynkin  34326  brfae  34407  sxbrsigalem3  34431  dya2icoseg2  34437  omsmeas  34482  sibfof  34499  sseqmw  34550  sseqf  34551  sseqp1  34554  fiblem  34557  fibp1  34560  probfinmeasbALTV  34588  repr0  34770  reprpmtf1o  34785  hgt750lemg  34813  bnj1379  34988  srcmpltd  35238  fineqvnttrclselem3  35281  subfacp1lem5  35380  subfacp1lem6  35381  cvxpconn  35438  cvxsconn  35439  cvmliftlem6  35486  cvmliftlem8  35488  cvmliftlem10  35490  cvmlift2lem6  35504  cvmlift2lem11  35509  cvmlift2lem12  35510  2goelgoanfmla1  35620  prv1n  35627  msubff  35726  msubco  35727  elmsta  35744  msubff1  35752  mvhf  35754  msubvrs  35756  iprodefisumlem  35936  filnetlem3  36576  knoppcnlem10  36704  knoppcnlem11  36705  icoreunrn  37566  icoreelrn  37568  ralssiun  37614  poimirlem3  37826  poimirlem16  37839  poimirlem17  37840  poimirlem19  37842  poimirlem30  37853  dvasin  37907  cover2  37918  upixp  37932  sdclem1  37946  fdc  37948  caushft  37964  ismtyres  38011  rrncmslem  38035  isfld2  38208  presuc  38693  osumcllem10N  40247  pexmidlem7N  40258  dihglblem2N  41576  lcfrvalsnN  41823  lcfrlem5  41828  lcfrlem6  41829  lcfrlem27  41851  lcfrlem37  41861  aks6d1c1p4  42387  aks6d1c1p7  42389  aks6d1c1p8  42391  evl1gprodd  42393  aks6d1c2lem4  42403  aks6d1c5lem3  42413  aks6d1c6lem2  42447  prjspvs  42874  0prjspnrel  42891  monotuz  43204  expdiophlem1  43284  kelac2  43328  naddwordnexlem4  43664  grurankcld  44495  dvgrat  44574  nzss  44579  uzmptshftfval  44608  binomcxplemnotnn0  44618  orbitinit  45218  orbitcl  45219  permaxinf2lem  45274  refsumcn  45296  rfcnpre2  45297  rfcnpre3  45299  rfcnpre4  45300  disjf1o  45456  unirnmap  45473  unirnmapsn  45479  ssmapsn  45481  mptssid  45506  allbutfi  45658  eluzd  45674  uzidd2  45681  ressiocsup  45821  ressioosup  45822  ressiooinf  45824  fsumsermpt  45846  climexp  45872  climinf  45873  climsuse  45875  sumnnodd  45897  limsupresico  45965  limsupubuzlem  45977  limsupresxr  46031  liminfresxr  46032  liminfresico  46036  limsup10exlem  46037  cnrefiisplem  46094  cncfiooicclem1  46158  dvsinax  46178  itgsinexplem1  46219  fvvolioof  46254  fvvolicof  46256  stoweidlem14  46279  stoweidlem16  46281  stoweidlem31  46296  stoweidlem34  46299  stoweidlem36  46301  stoweidlem43  46308  stoweidlem46  46311  stoweidlem47  46312  stoweidlem52  46317  stoweidlem55  46320  stoweidlem57  46322  dirkercncf  46372  fourierdlem20  46392  fourierdlem42  46414  fourierdlem48  46419  fourierdlem49  46420  fourierdlem51  46422  fourierdlem54  46425  fourierdlem62  46433  fourierdlem71  46442  fourierdlem80  46451  fourierdlem114  46485  fouriersw  46496  ioorrnopnlem  46569  ioorrnopnxrlem  46571  salexct3  46607  salgencntex  46608  salgensscntex  46609  subsalsal  46624  sge0fodjrnlem  46681  sge0isum  46692  sge0seq  46711  sge0reuz  46712  sge0reuzb  46713  meadjiunlem  46730  meaiininclem  46751  carageniuncllem1  46786  caratheodorylem1  46791  hoiprodp1  46853  hoidmv1lelem1  46856  hoidmv1lelem2  46857  hoidmv1le  46859  hoidmvlelem1  46860  hoidmvlelem2  46861  hoidmvlelem3  46862  voncmpl  46886  hoiqssbl  46890  smflimlem2  47037  smfsuplem1  47076  smfsuplem3  47078  fsupdm  47107  finfdm  47111  cfsetsnfsetf  47325  fcores  47334  afvres  47439  afv2res  47506  fundcmpsurinjimaid  47678  iccpartigtl  47690  sprsymrelf  47762  prproropf1olem2  47771  uhgrimedgi  48157  isuspgrim0lem  48160  isuspgrimlem  48162  ushggricedg  48194  grimedg  48202  usgrgrtrirex  48217  isubgr3stgrlem7  48239  uspgrlimlem4  48258  grlimprclnbgr  48263  gpgiedgdmellem  48313  gpg3kgrtriex  48356  funcringcsetcALTV2lem3  48559  funcringcsetclem3ALTV  48582  lindslinindsimp2lem5  48729  rrxsphere  49015  line2  49019  iooii  49184  icccldii  49185  iscnrm3rlem3  49208  eloppf2  49400  oppcup  49473  natoppf  49495  zeroo2  49500  oppfdiag1  49680  oppfdiag  49682  2arwcat  49866  incat  49867  lmddu  49933  onsetreclem3  49973  amgmwlem  50068