Theorem eleqtrrdi 2875

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2839

This theorem is used by:  3eltr4g  2881  srcmpltd  4435  brelrng  5928  elabrex  7256  elabrexg  7257  fliftel1  7328  ovidig  7572  unielxp  8049  tfrlem11  8410  rdglim  8448  seqomlem4  8477  2oconcl  8525  ecopqsi  8805  erov  8849  eroprf  8850  sbthlem2  9121  dffi3  9436  ixpiunwdom  9597  cantnfcl  9681  r1lim  9792  rankwflembOLD  9814  pwwf  9828  unwf  9831  rankwflem  9837  uniwf  9841  rankpwi  9845  rankr1g  9857  r1pw  9872  r1rankid  9888  rankuni  9892  elhf4  9925  djulcl  10004  djurcl  10005  inlresf  10008  inrresf  10010  djuun  10020  cardlim  10066  infxpenlem  10105  alephfp  10200  cfsmolem  10361  alephsing  10367  hsmexlem4  10520  axdc3lem2  10542  numth3  10561  iunfo  10636  konigthlem  10666  iunctb  10672  canthwelem  10748  canthwe  10749  r1limwun  10834  inar1  10873  inatsk  10876  gruina  10916  grur1  10918  tskmval  10937  tskmcl  10939  pinq  11025  dmrecnq  11066  addclsr  11181  mulclsr  11182  axaddf  11243  axmulf  11244  peano2nn  12360  uztrn2  12997  eluz2nn  13028  peano2uzs  13042  uzsupss  13080  uzsup  14016  uzrdgfni  14114  uzrdgsuci  14116  fsuppmapnn0fiub  14147  seqf  14179  ser0  14210  bcm1k  14472  bcp1nk  14474  bcpasc  14478  hashprdifel  14555  fz1isolem  14619  pr2pwpr  14637  tpf  14657  ccats1val2  14789  rexuzre  15535  limsupgre  15663  climconst  15725  rlimclim1  15727  climrlim2  15729  clim2ser  15837  clim2ser2  15838  iserex  15839  isermulc2  15840  iserle  15842  isercolllem3  15849  isercoll2  15851  climsup  15852  iseraltlem2  15865  iseraltlem3  15866  zsum  15899  isumclim3  15940  isumadd  15948  fsump1i  15950  iserabs  15997  cvgcmp  15998  cvgcmpub  15999  cvgcmpce  16000  abscvgcvg  16001  isumshft  16023  isumsplit  16024  isum1p  16025  isumrpcl  16027  isumsup2  16030  climcndslem1  16033  cvgrat  16067  clim2prod  16072  clim2div  16073  prodf1  16075  ntrivcvgn0  16082  ntrivcvgtail  16084  fprodntriv  16124  fprodabs  16156  fprodeq0  16157  iprodclim3  16182  iprodmul  16185  ef0lem  16259  fprodefsum  16276  rpnnen2lem3  16399  dvdsflip  16502  fzo0dvdseq  16508  bitsinv1  16627  smupval  16673  smueqlem  16675  seq1st  16761  algr0  16762  prmind2  16875  crth  16970  eulerthlem2  16974  prmdiv  16977  pockthlem  17098  pockthg  17099  unbenlem  17101  prmunb  17107  prmgaplem7  17250  strfv2d  17394  imasvscaval  17725  oppccatid  17908  oppccatf  17917  epii  17933  fthepi  18120  funcestrcsetclem3  18331  funcsetcestrclem3  18345  yon12  18454  yon2  18455  yonedalem4c  18466  yonedalem22  18467  yonedalem3b  18468  yonedainv  18470  acsmapd  18743  chnub  18811  chnccats1  18814  chnccat  18815  mgm2nsgrplem1  19132  mgm2nsgrplem2  19133  mgm2nsgrplem3  19134  sgrp2nmndlem1  19137  sgrp2rid2  19140  ghmqusker  19516  cntrsubgnsg  19572  symgpssefmnd  19625  pmtrrn  19686  gexcl3  19816  efgi  19948  efgi2  19954  efgs1b  19965  efgredlemg  19971  efgredlemd  19973  frgpnabllem1  20102  cycsubgcyg  20130  gsumzaddlem  20150  dprdwd  20242  dprd2da  20273  rhmopp  20774  lsppratlem3  21442  lsppratlem4  21443  lbsextlem2  21452  lidl0ALT  21523  lidl1ALT  21526  2idl0  21569  2idl1  21570  rhmpreimaprmidl  21650  ssdifidllem  21655  ssdifidl  21656  domnchr  21853  znf1o  21872  mplsubrglem  22326  mpfconst  22433  mpfproj  22434  mpfind  22439  mhpmulcl  22485  pf1const  22679  pf1id  22680  mpfpf1  22684  pf1mpf  22685  madetsumid  22791  slesolex  23015  pmatcoe1fsupp  23034  mat2pmatbas0  23060  pmatcollpw  23114  pm2mpf1  23132  isclo  23420  indiscld  23424  restntr  23515  ordtbaslem  23521  ordtbas2  23524  lmconst  23594  lmss  23631  conncompid  23764  2ndcomap  23792  locfincmp  23860  comppfsc  23866  xkouni  23933  txcls  23938  ptclsg  23949  uptx  23959  txindis  23968  tx1stc  23984  cnmpt1res  24010  tgqtop  24046  uffix  24255  cnpflf2  24334  ptcmplem2  24387  ptcmplem4  24389  tgpconncomp  24447  tsmsfbas  24462  fmucnd  24625  prdsxmetlem  24702  imasdsf1olem  24707  prdsbl  24825  blcvx  25132  xrsmopn  25147  xrge0tsms  25169  metdcn2  25174  expcncf  25262  cnmpopc  25264  icchmeo  25277  iccpnfhmeo  25281  cnheibor  25291  evth  25295  evth2  25296  lebnumlem2  25298  lebnumii  25302  reparphti  25333  cfilfcls  25610  minveclem2  25762  minveclem3  25765  minveclem4  25768  ovoliunlem1  25838  ovolicc1  25852  iundisj  25884  volsup  25892  uniioombllem3  25921  vitalilem2  25945  vitalilem3  25946  mbfsup  26000  mbfinf  26001  mbflimsup  26002  itg2monolem1  26086  limcflflem  26215  limccnp  26226  limccnp2  26227  dvidlem  26250  dvn2bss  26265  cpnres  26272  dvcobr  26281  dvrec  26290  c1liplem1  26331  dvcnvrelem2  26353  dvfsumrlimf  26360  dvfsumlem1  26361  dvfsumlem2  26362  dvfsumlem3  26363  dvfsumlem4  26364  dvfsumrlim  26366  dvfsum2  26369  coeeulem  26558  coeid3  26574  plycn  26595  dvntaylp  26713  taylthlem1  26715  taylthlem2  26716  ulm2  26727  ulmshftlem  26731  ulmshft  26732  ulm0  26733  ulmcn  26741  ulmdvlem3  26744  ulmdv  26745  mtest  26746  mtestbdd  26747  dvradcnv  26763  psercn2  26765  psercn  26768  pserdv  26771  abelth  26783  efif1olem2  26886  efif1olem4  26888  efifo  26890  eff1olem  26891  logcn  26990  dvloglem  26991  cxpcn3  27091  resqrtcn  27092  sqrtcn  27093  logbleb  27126  logblt  27127  asinneg  27229  atanlogsub  27259  atanbnd  27269  ressatans  27277  leibpilem2  27284  xrlimcnp  27311  efrlim  27312  scvxcvx  27328  ppiub  27546  chtub  27554  logexprlim  27567  lgseisenlem1  27717  rplogsumlem1  27826  rplogsumlem2  27827  dchrisumlem2  27832  dchrisum0flb  27852  logdivbnd  27898  pntlem3  27951  dfnns2  28773  tgcgr4  29009  ltgov  29075  elcgrabasrd  29391  cgrabasimass  29393  f1otrg  29463  eengtrkg  29579  iedgedg  29643  ushgredgedgloop  29827  subgruhgredgd  29880  uvtxupgrres  30004  umgr2v2evd2  30123  edginwlk  30230  wlk1walk  30234  crctcshwlkn0lem6  30419  wlkiswwlks1  30471  minvecolem1  31491  minvecolem2  31492  minvecolem4  31497  htthlem  31534  5oalem2  32272  3oalem2  32280  iundisjf  33240  fmptco1f1o  33284  xppreima  33296  xppreima2  33302  dfcnv2  33326  ccatws1f1o  33570  gsumhashmul  33684  xrge0tsmsd  33690  gsumwrd2dccatlem  33694  odpmco  33703  pmtrcnelor  33708  fzo0pmtrlast  33709  wrdpmtrlast  33710  pmtrto1cl  33716  psgnfzto1stlem  33717  fzto1stfv1  33718  fzto1st  33720  fzto1stinvn  33721  psgnfzto1st  33722  tocycf  33734  cycpmco2lem7  33749  cycpmco2  33750  cycpmrn  33760  cyc3evpm  33767  cyc3genpmlem  33768  cycpmgcl  33770  cyc3conja  33774  elrgspnlem1  33859  elrgspnlem2  33860  elrgspnlem3  33861  elrgspnlem4  33862  elrgspnsubrunlem1  33864  nsgmgc  34019  nsgqusf1olem1  34020  nsgqusf1olem2  34021  ssmxidllem  34054  drngmxidlr  34058  opprqus1r  34072  qsdrngilem  34074  qsdrngi  34075  rsprprmprmidlb  34111  rprmirredb  34120  1arithufdlem1  34132  1arithufdlem2  34133  1arithufdlem3  34134  1arithufdlem4  34135  fply1  34146  ply1degltel  34182  ply1degleel  34183  ply1degltlss  34184  mplmulmvr  34227  psrmon  34237  psrmonprod  34240  esplylem  34254  esplyfv1  34257  esplysply  34259  esplyind  34263  ply1degltdimlem  34310  ply1degltdim  34311  algextdeglem4  34408  algextdeglem6  34410  algextdeglem7  34411  algextdeglem8  34412  nn0constr  34449  smatlem  34485  smatcl  34490  zartopn  34563  zarmxt1  34568  tpr2rico  34600  xrmulc1cn  34618  xrge0mulc1cn  34629  esumpfinvallem  34762  ldgenpisyslem1  34852  dynkin  34856  brfae  34937  sxbrsigalem3  34960  dya2icoseg2  34966  omsmeas  35011  sibfof  35028  sseqmw  35079  sseqf  35080  sseqp1  35083  fiblem  35086  fibp1  35089  probfinmeasbALTV  35117  repr0  35296  reprpmtf1o  35311  hgt750lemg  35339  bnj1379  35516  fineqvnttrclselem3  35865  subfacp1lem5  36073  subfacp1lem6  36074  cvxpconn  36131  cvxsconn  36132  cvmliftlem6  36179  cvmliftlem8  36181  cvmliftlem10  36183  cvmlift2lem6  36197  cvmlift2lem11  36202  cvmlift2lem12  36203  2goelgoanfmla1  36313  prv1n  36320  msubff  36419  msubco  36420  elmsta  36437  msubff1  36445  mvhf  36447  msubvrs  36449  onprcr  36586  iprodefisumlem  36635  filnetlem3  37298  ttcid  37410  ttcwf  37442  knoppcnlem10  37498  knoppcnlem11  37499  icoreunrn  38425  icoreelrn  38427  ralssiun  38473  poimirlem3  38684  poimirlem16  38697  poimirlem17  38698  poimirlem19  38700  poimirlem30  38711  dvasin  38765  varprop  38785  negprop  38786  impprop  38787  cover2  38792  upixp  38806  sdclem1  38820  fdc  38822  caushft  38838  ismtyres  38885  rrncmslem  38909  isfld2  39082  presuc  39573  osumcllem10N  41165  pexmidlem7N  41176  dihglblem2N  42494  lcfrvalsnN  42741  lcfrlem5  42746  lcfrlem6  42747  lcfrlem27  42769  lcfrlem37  42779  aks6d1c1p4  43304  aks6d1c1p7  43306  aks6d1c1p8  43308  evl1gprodd  43310  aks6d1c2lem4  43320  aks6d1c5lem3  43330  aks6d1c6lem2  43364  prjspvs  43781  frlmnzcoordsca  43801  prjspnnorm  43804  0prjspnrel  43806  monotuz  44091  expdiophlem1  44171  kelac2  44210  naddwordnexlem4  44546  grurankcld  45374  dvgrat  45439  nzss  45444  uzmptshftfval  45473  binomcxplemnotnn0  45483  orbitinit  46088  orbitcl  46089  permaxinf2lem  46144  ishfstruct  46170  refsumcn  46189  rfcnpre2  46190  rfcnpre3  46192  rfcnpre4  46193  disjf1o  46348  unirnmap  46363  unirnmapsn  46369  ssmapsn  46371  mptssid  46395  allbutfi  46546  eluzd  46561  uzidd2  46568  ressiocsup  46708  ressioosup  46709  ressiooinf  46711  fsumsermpt  46733  climexp  46759  climinf  46760  climsuse  46762  limsupresico  46852  limsupubuzlem  46864  limsupresxr  46918  liminfresxr  46919  liminfresico  46923  limsup10exlem  46924  cnrefiisplem  46981  cncfiooicclem1  47045  dvsinax  47065  itgsinexplem1  47106  fvvolioof  47141  fvvolicof  47143  stoweidlem14  47166  stoweidlem16  47168  stoweidlem31  47183  stoweidlem34  47186  stoweidlem36  47188  stoweidlem43  47195  stoweidlem46  47198  stoweidlem47  47199  stoweidlem52  47204  stoweidlem55  47207  stoweidlem57  47209  dirkercncf  47259  fourierdlem20  47279  fourierdlem42  47301  fourierdlem51  47309  fourierdlem54  47312  fourierdlem62  47320  fourierdlem71  47329  fourierdlem80  47338  fourierdlem114  47372  fouriersw  47383  ioorrnopnlem  47456  ioorrnopnxrlem  47458  salexct3  47494  salgencntex  47495  salgensscntex  47496  subsalsal  47511  sge0fodjrnlem  47568  sge0isum  47579  sge0seq  47598  sge0reuz  47599  sge0reuzb  47600  meadjiunlem  47617  meaiininclem  47638  carageniuncllem1  47673  caratheodorylem1  47678  hoiprodp1  47740  hoidmv1lelem1  47743  hoidmv1lelem2  47744  hoidmv1le  47746  hoidmvlelem1  47747  hoidmvlelem2  47748  hoidmvlelem3  47749  voncmpl  47773  hoiqssbl  47777  smflimlem2  47924  smfsuplem1  47963  smfsuplem3  47965  fsupdm  47994  finfdm  47998  sinnpoly  48083  cfsetsnfsetf  48270  fcores  48279  afvres  48384  afv2res  48451  fundcmpsurinjimaid  48635  iccpartigtl  48647  sprsymrelf  48719  prproropf1olem2  48728  uhgrimedgi  49130  isuspgrim0lem  49133  isuspgrimlem  49135  ushggricedg  49167  grimedg  49175  usgrgrtrirex  49190  isubgr3stgrlem7  49212  uspgrlimlem4  49231  grlimprclnbgr  49236  gpgiedgdmellem  49286  gpg3kgrtriex  49329  funcringcsetcALTV2lem3  49531  funcringcsetclem3ALTV  49554  lindslinindsimp2lem5  49716  prelrrx2  49967  prelrrx2bd  49968  rrxsphere  50002  line2  50006  iooii  50174  icccldii  50175  iscnrm3rlem3  50198  eloppf2  50392  oppcup  50465  natoppf  50493  zeroo2  50498  oppfdiag1  50691  oppfdiag  50693  2arwcat  50880  incat  50881  parhomcl2  50887  parswapprop  50919  lmddu  50992  onsetreclem3  51017  amgmwlem  51204