Theorem eleqtrrdi 2874

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

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-clel 2838

This theorem is referenced by:  3eltr4g  2880  brelrng  5918  elabrex  7227  elabrexg  7228  fliftel1  7295  ovidig  7539  unielxp  8009  tfrlem11  8360  rdglim  8398  seqomlem4  8425  2oconcl  8473  ecopqsi  8753  erov  8797  eroprf  8798  sbthlem2  9061  dffi3  9378  ixpiunwdom  9539  cantnfcl  9623  r1lim  9731  rankwflemb  9752  pwwf  9766  unwf  9769  rankwflem  9774  uniwf  9778  rankpwi  9782  rankr1g  9791  r1pw  9804  r1rankid  9818  rankuni  9822  djulcl  9869  djurcl  9870  inlresf  9873  inrresf  9875  djuun  9885  cardlim  9931  infxpenlem  9970  alephfp  10065  cfsmolem  10228  alephsing  10234  hsmexlem4  10387  axdc3lem2  10409  numth3  10428  iunfo  10497  konigthlem  10527  iunctb  10533  canthwelem  10609  canthwe  10610  r1limwun  10695  inar1  10734  inatsk  10737  gruina  10777  grur1  10779  tskmval  10798  tskmcl  10800  pinq  10886  dmrecnq  10927  addclsr  11042  mulclsr  11043  axaddf  11104  axmulf  11105  peano2nn  12223  uztrn2  12859  eluz2nn  12890  peano2uzs  12904  uzsupss  12942  uzsup  13874  uzrdgfni  13972  uzrdgsuci  13974  fsuppmapnn0fiub  14005  seqf  14037  ser0  14068  bcm1k  14329  bcp1nk  14331  bcpasc  14335  hashprdifel  14412  fz1isolem  14475  pr2pwpr  14493  tpf  14513  ccats1val2  14642  rexuzre  15381  limsupgre  15509  climconst  15571  rlimclim1  15573  climrlim2  15575  clim2ser  15683  clim2ser2  15684  iserex  15685  isermulc2  15686  iserle  15688  isercolllem3  15695  isercoll2  15697  climsup  15698  iseraltlem2  15711  iseraltlem3  15712  zsum  15746  isumclim3  15787  isumadd  15795  fsump1i  15797  iserabs  15844  cvgcmp  15845  cvgcmpub  15846  cvgcmpce  15847  abscvgcvg  15848  isumshft  15870  isumsplit  15871  isum1p  15872  isumrpcl  15874  isumsup2  15877  climcndslem1  15880  cvgrat  15914  clim2prod  15919  clim2div  15920  prodf1  15922  ntrivcvgn0  15929  ntrivcvgtail  15931  fprodntriv  15973  fprodabs  16005  fprodeq0  16006  iprodclim3  16031  iprodmul  16034  ef0lem  16109  fprodefsum  16126  rpnnen2lem3  16249  dvdsflip  16352  fzo0dvdseq  16358  bitsinv1  16477  smupval  16523  smueqlem  16525  seq1st  16606  algr0  16607  prmind2  16720  crth  16814  eulerthlem2  16818  prmdiv  16821  pockthlem  16942  pockthg  16943  unbenlem  16945  prmunb  16951  prmgaplem7  17094  strfv2d  17238  imasvscaval  17569  oppccatid  17752  oppccatf  17761  epii  17777  fthepi  17964  funcestrcsetclem3  18175  funcsetcestrclem3  18189  yon12  18298  yon2  18299  yonedalem4c  18310  yonedalem22  18311  yonedalem3b  18312  yonedainv  18314  acsmapd  18587  chnub  18655  chnccats1  18658  chnccat  18659  mgm2nsgrplem1  18956  mgm2nsgrplem2  18957  mgm2nsgrplem3  18958  sgrp2nmndlem1  18961  sgrp2rid2  18964  ghmqusker  19328  cntrsubgnsg  19384  symgpssefmnd  19437  pmtrrn  19498  gexcl3  19628  efgi  19760  efgi2  19766  efgs1b  19777  efgredlemg  19783  efgredlemd  19785  frgpnabllem1  19914  cycsubgcyg  19942  gsumzaddlem  19962  dprdwd  20054  dprd2da  20085  rhmopp  20560  lsppratlem3  21220  lsppratlem4  21221  lbsextlem2  21230  lidl0ALT  21299  lidl1ALT  21302  2idl0  21331  2idl1  21332  domnchr  21585  znf1o  21604  mplsubrglem  22056  mpfconst  22163  mpfproj  22164  mpfind  22169  mhpmulcl  22215  pf1const  22410  pf1id  22411  mpfpf1  22415  pf1mpf  22416  madetsumid  22522  slesolex  22743  pmatcoe1fsupp  22762  mat2pmatbas0  22788  pmatcollpw  22842  pm2mpf1  22860  isclo  23148  indiscld  23152  restntr  23243  ordtbaslem  23249  ordtbas2  23252  lmconst  23322  lmss  23359  conncompid  23492  2ndcomap  23519  locfincmp  23587  comppfsc  23593  xkouni  23660  txcls  23665  ptclsg  23676  uptx  23686  txindis  23695  tx1stc  23711  cnmpt1res  23737  tgqtop  23773  uffix  23982  cnpflf2  24061  ptcmplem2  24114  ptcmplem4  24116  tgpconncomp  24174  tsmsfbas  24189  fmucnd  24352  prdsxmetlem  24429  imasdsf1olem  24434  prdsbl  24552  blcvx  24859  xrsmopn  24874  xrge0tsms  24896  metdcn2  24901  expcncf  24989  cnmpopc  24991  icchmeo  25004  iccpnfhmeo  25008  cnheibor  25018  evth  25022  evth2  25023  lebnumlem2  25025  lebnumii  25029  reparphti  25060  cfilfcls  25337  minveclem2  25489  minveclem3  25492  minveclem4  25495  ovoliunlem1  25565  ovolicc1  25579  iundisj  25611  volsup  25619  uniioombllem3  25648  vitalilem2  25672  vitalilem3  25673  mbfsup  25727  mbfinf  25728  mbflimsup  25729  itg2monolem1  25813  limcflflem  25943  limccnp  25954  limccnp2  25955  dvidlem  25978  dvn2bss  25993  cpnres  26000  dvcobr  26009  dvrec  26018  c1liplem1  26059  dvcnvrelem2  26081  dvfsumrlimf  26088  dvfsumlem1  26089  dvfsumlem2  26090  dvfsumlem3  26091  dvfsumlem4  26092  dvfsumrlim  26094  dvfsum2  26097  coeeulem  26285  coeid3  26301  plycn  26322  dvntaylp  26435  taylthlem1  26437  taylthlem2  26438  ulm2  26449  ulmshftlem  26453  ulmshft  26454  ulm0  26455  ulmcn  26463  ulmdvlem3  26466  ulmdv  26467  mtest  26468  mtestbdd  26469  dvradcnv  26485  psercn2  26487  psercn  26490  pserdv  26493  abelth  26505  efif1olem2  26609  efif1olem4  26611  efifo  26613  eff1olem  26614  logcn  26713  dvloglem  26714  cxpcn3  26814  resqrtcn  26815  sqrtcn  26816  logbleb  26849  logblt  26850  asinneg  26952  atanlogsub  26982  atanbnd  26992  ressatans  27000  leibpilem2  27007  xrlimcnp  27034  efrlim  27035  scvxcvx  27051  ppiub  27269  chtub  27277  logexprlim  27290  lgseisenlem1  27440  rplogsumlem1  27549  rplogsumlem2  27550  dchrisumlem2  27555  dchrisum0flb  27575  logdivbnd  27621  pntlem3  27674  dfnns2  28466  tgcgr4  28701  ltgov  28767  f1otrg  29072  eengtrkg  29188  iedgedg  29252  ushgredgedgloop  29433  subgruhgredgd  29486  uvtxupgrres  29610  umgr2v2evd2  29729  edginwlk  29836  wlk1walk  29840  crctcshwlkn0lem6  30016  wlkiswwlks1  30068  minvecolem1  31078  minvecolem2  31079  minvecolem4  31084  htthlem  31121  5oalem2  31859  3oalem2  31867  iundisjf  32790  fmptco1f1o  32836  xppreima  32848  xppreima2  32854  dfcnv2  32878  ccatws1f1o  33130  gsumhashmul  33248  xrge0tsmsd  33254  gsumwrd2dccatlem  33258  odpmco  33267  pmtrcnelor  33272  fzo0pmtrlast  33273  wrdpmtrlast  33274  pmtrto1cl  33280  psgnfzto1stlem  33281  fzto1stfv1  33282  fzto1st  33284  fzto1stinvn  33285  psgnfzto1st  33286  tocycf  33298  cycpmco2lem7  33313  cycpmco2  33314  cycpmrn  33324  cyc3evpm  33331  cyc3genpmlem  33332  cycpmgcl  33334  cyc3conja  33338  elrgspnlem1  33424  elrgspnlem2  33425  elrgspnlem3  33426  elrgspnlem4  33427  elrgspnsubrunlem1  33429  nsgmgc  33599  nsgqusf1olem1  33600  nsgqusf1olem2  33601  rhmpreimaprmidl  33639  ssdifidllem  33644  ssdifidl  33645  ssmxidllem  33662  drngmxidlr  33667  opprqus1r  33681  qsdrngilem  33683  qsdrngi  33684  rsprprmprmidlb  33720  rprmirredb  33729  1arithufdlem1  33741  1arithufdlem2  33742  1arithufdlem3  33743  1arithufdlem4  33744  fply1  33755  ply1degltel  33791  ply1degleel  33792  ply1degltlss  33793  mplmulmvr  33837  psrmon  33847  psrmonprod  33850  esplylem  33864  esplyfv1  33867  esplysply  33869  esplyind  33873  ply1degltdimlem  33920  ply1degltdim  33921  algextdeglem4  34018  algextdeglem6  34020  algextdeglem7  34021  algextdeglem8  34022  nn0constr  34059  smatlem  34095  smatcl  34100  zartopn  34173  zarmxt1  34178  tpr2rico  34210  xrmulc1cn  34228  xrge0mulc1cn  34239  esumpfinvallem  34372  ldgenpisyslem1  34461  dynkin  34465  brfae  34546  sxbrsigalem3  34570  dya2icoseg2  34576  omsmeas  34621  sibfof  34638  sseqmw  34689  sseqf  34690  sseqp1  34693  fiblem  34696  fibp1  34699  probfinmeasbALTV  34727  repr0  34906  reprpmtf1o  34921  hgt750lemg  34949  bnj1379  35126  srcmpltd  35376  fineqvnttrclselem3  35420  subfacp1lem5  35535  subfacp1lem6  35536  cvxpconn  35593  cvxsconn  35594  cvmliftlem6  35641  cvmliftlem8  35643  cvmliftlem10  35645  cvmlift2lem6  35659  cvmlift2lem11  35664  cvmlift2lem12  35665  2goelgoanfmla1  35775  prv1n  35782  msubff  35881  msubco  35882  elmsta  35899  msubff1  35907  mvhf  35909  msubvrs  35911  iprodefisumlem  36091  filnetlem3  36741  ttcid  36853  ttcwf  36885  knoppcnlem10  36941  knoppcnlem11  36942  icoreunrn  37854  icoreelrn  37856  ralssiun  37902  poimirlem3  38123  poimirlem16  38136  poimirlem17  38137  poimirlem19  38139  poimirlem30  38150  dvasin  38204  cover2  38215  upixp  38229  sdclem1  38243  fdc  38245  caushft  38261  ismtyres  38308  rrncmslem  38332  isfld2  38505  presuc  38998  osumcllem10N  40590  pexmidlem7N  40601  dihglblem2N  41919  lcfrvalsnN  42166  lcfrlem5  42171  lcfrlem6  42172  lcfrlem27  42194  lcfrlem37  42204  aks6d1c1p4  42729  aks6d1c1p7  42731  aks6d1c1p8  42733  evl1gprodd  42735  aks6d1c2lem4  42745  aks6d1c5lem3  42755  aks6d1c6lem2  42789  prjspvs  43193  0prjspnrel  43210  monotuz  43519  expdiophlem1  43599  kelac2  43643  naddwordnexlem4  43979  grurankcld  44810  dvgrat  44889  nzss  44894  uzmptshftfval  44923  binomcxplemnotnn0  44933  orbitinit  45533  orbitcl  45534  permaxinf2lem  45589  refsumcn  45611  rfcnpre2  45612  rfcnpre3  45614  rfcnpre4  45615  disjf1o  45770  unirnmap  45785  unirnmapsn  45791  ssmapsn  45793  mptssid  45817  allbutfi  45969  eluzd  45984  uzidd2  45991  ressiocsup  46131  ressioosup  46132  ressiooinf  46134  fsumsermpt  46156  climexp  46182  climinf  46183  climsuse  46185  sumnnodd  46207  limsupresico  46275  limsupubuzlem  46287  limsupresxr  46341  liminfresxr  46342  liminfresico  46346  limsup10exlem  46347  cnrefiisplem  46404  cncfiooicclem1  46468  dvsinax  46488  itgsinexplem1  46529  fvvolioof  46564  fvvolicof  46566  stoweidlem14  46589  stoweidlem16  46591  stoweidlem31  46606  stoweidlem34  46609  stoweidlem36  46611  stoweidlem43  46618  stoweidlem46  46621  stoweidlem47  46622  stoweidlem52  46627  stoweidlem55  46630  stoweidlem57  46632  dirkercncf  46682  fourierdlem20  46702  fourierdlem42  46724  fourierdlem51  46732  fourierdlem54  46735  fourierdlem62  46743  fourierdlem71  46752  fourierdlem80  46761  fourierdlem114  46795  fouriersw  46806  ioorrnopnlem  46879  ioorrnopnxrlem  46881  salexct3  46917  salgencntex  46918  salgensscntex  46919  subsalsal  46934  sge0fodjrnlem  46991  sge0isum  47002  sge0seq  47021  sge0reuz  47022  sge0reuzb  47023  meadjiunlem  47040  meaiininclem  47061  carageniuncllem1  47096  caratheodorylem1  47101  hoiprodp1  47163  hoidmv1lelem1  47166  hoidmv1lelem2  47167  hoidmv1le  47169  hoidmvlelem1  47170  hoidmvlelem2  47171  hoidmvlelem3  47172  voncmpl  47196  hoiqssbl  47200  smflimlem2  47347  smfsuplem1  47386  smfsuplem3  47388  fsupdm  47417  finfdm  47421  cfsetsnfsetf  47653  fcores  47662  afvres  47767  afv2res  47834  fundcmpsurinjimaid  48018  iccpartigtl  48030  sprsymrelf  48102  prproropf1olem2  48111  uhgrimedgi  48513  isuspgrim0lem  48516  isuspgrimlem  48518  ushggricedg  48550  grimedg  48558  usgrgrtrirex  48573  isubgr3stgrlem7  48595  uspgrlimlem4  48614  grlimprclnbgr  48619  gpgiedgdmellem  48669  gpg3kgrtriex  48712  funcringcsetcALTV2lem3  48915  funcringcsetclem3ALTV  48938  lindslinindsimp2lem5  49085  rrxsphere  49371  line2  49375  iooii  49540  icccldii  49541  iscnrm3rlem3  49564  eloppf2  49756  oppcup  49829  natoppf  49851  zeroo2  49856  oppfdiag1  50036  oppfdiag  50038  2arwcat  50222  incat  50223  lmddu  50289  onsetreclem3  50329  amgmwlem  50424