Theorem eleqtrrdi 2850

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  3eltr4g  2856  brelrng  5884  elabrex  7187  elabrexg  7188  fliftel1  7255  ovidig  7499  unielxp  7970  tfrlem11  8318  rdglim  8356  seqomlem4  8383  2oconcl  8429  ecopqsi  8708  erov  8752  eroprf  8753  sbthlem2  9017  dffi3  9335  ixpiunwdom  9496  cantnfcl  9580  r1lim  9688  rankwflemb  9709  pwwf  9723  unwf  9726  rankwflem  9731  uniwf  9735  rankpwi  9739  rankr1g  9748  r1pw  9761  r1rankid  9775  rankuni  9779  djulcl  9826  djurcl  9827  inlresf  9830  inrresf  9832  djuun  9842  cardlim  9888  infxpenlem  9927  alephfp  10022  cfsmolem  10184  alephsing  10190  hsmexlem4  10343  axdc3lem2  10365  numth3  10384  iunfo  10453  konigthlem  10483  iunctb  10489  canthwelem  10565  canthwe  10566  r1limwun  10651  inar1  10690  inatsk  10693  gruina  10733  grur1  10735  tskmval  10754  tskmcl  10756  pinq  10842  dmrecnq  10883  addclsr  10998  mulclsr  10999  axaddf  11060  axmulf  11061  peano2nn  12178  uztrn2  12799  eluz2nn  12830  peano2uzs  12844  uzsupss  12882  uzsup  13814  uzrdgfni  13912  uzrdgsuci  13914  fsuppmapnn0fiub  13945  seqf  13977  ser0  14008  bcm1k  14269  bcp1nk  14271  bcpasc  14275  hashprdifel  14352  fz1isolem  14415  pr2pwpr  14433  tpf  14453  ccats1val2  14582  rexuzre  15307  limsupgre  15435  climconst  15497  rlimclim1  15499  climrlim2  15501  clim2ser  15609  clim2ser2  15610  iserex  15611  isermulc2  15612  iserle  15614  isercolllem3  15621  isercoll2  15623  climsup  15624  iseraltlem2  15637  iseraltlem3  15638  zsum  15672  isumclim3  15713  isumadd  15721  fsump1i  15723  iserabs  15770  cvgcmp  15771  cvgcmpub  15772  cvgcmpce  15773  abscvgcvg  15774  isumshft  15796  isumsplit  15797  isum1p  15798  isumrpcl  15800  isumsup2  15803  climcndslem1  15806  cvgrat  15840  clim2prod  15845  clim2div  15846  prodf1  15848  ntrivcvgn0  15855  ntrivcvgtail  15857  fprodntriv  15899  fprodabs  15931  fprodeq0  15932  iprodclim3  15957  iprodmul  15960  ef0lem  16035  fprodefsum  16052  rpnnen2lem3  16175  dvdsflip  16278  fzo0dvdseq  16284  bitsinv1  16403  smupval  16449  smueqlem  16451  seq1st  16532  algr0  16533  prmind2  16646  crth  16740  eulerthlem2  16744  prmdiv  16747  pockthlem  16868  pockthg  16869  unbenlem  16871  prmunb  16877  prmgaplem7  17020  strfv2d  17163  imasvscaval  17494  oppccatid  17677  oppccatf  17686  epii  17702  fthepi  17889  funcestrcsetclem3  18100  funcsetcestrclem3  18114  yon12  18223  yon2  18224  yonedalem4c  18235  yonedalem22  18236  yonedalem3b  18237  yonedainv  18239  acsmapd  18512  chnub  18580  chnccats1  18583  chnccat  18584  mgm2nsgrplem1  18881  mgm2nsgrplem2  18882  mgm2nsgrplem3  18883  sgrp2nmndlem1  18886  sgrp2rid2  18889  ghmqusker  19254  cntrsubgnsg  19310  symgpssefmnd  19363  pmtrrn  19424  gexcl3  19554  efgi  19686  efgi2  19692  efgs1b  19703  efgredlemg  19709  efgredlemd  19711  frgpnabllem1  19840  cycsubgcyg  19868  gsumzaddlem  19888  dprdwd  19980  dprd2da  20011  rhmopp  20482  lsppratlem3  21143  lsppratlem4  21144  lbsextlem2  21153  lidl0ALT  21222  lidl1ALT  21225  2idl0  21254  2idl1  21255  domnchr  21508  znf1o  21527  mplsubrglem  21979  mpfconst  22086  mpfproj  22087  mpfind  22092  mhpmulcl  22138  pf1const  22333  pf1id  22334  mpfpf1  22338  pf1mpf  22339  madetsumid  22445  slesolex  22666  pmatcoe1fsupp  22685  mat2pmatbas0  22711  pmatcollpw  22765  pm2mpf1  22783  isclo  23071  indiscld  23075  restntr  23166  ordtbaslem  23172  ordtbas2  23175  lmconst  23245  lmss  23282  conncompid  23415  2ndcomap  23442  locfincmp  23510  comppfsc  23516  xkouni  23583  txcls  23588  ptclsg  23599  uptx  23609  txindis  23618  tx1stc  23634  cnmpt1res  23660  tgqtop  23696  uffix  23905  cnpflf2  23984  ptcmplem2  24037  ptcmplem4  24039  tgpconncomp  24097  tsmsfbas  24112  fmucnd  24275  prdsxmetlem  24352  imasdsf1olem  24357  prdsbl  24475  blcvx  24782  xrsmopn  24797  xrge0tsms  24819  metdcn2  24824  expcncf  24912  cnmpopc  24914  icchmeo  24927  iccpnfhmeo  24931  cnheibor  24941  evth  24945  evth2  24946  lebnumlem2  24948  lebnumii  24952  reparphti  24983  cfilfcls  25260  minveclem2  25412  minveclem3  25415  minveclem4  25418  ovoliunlem1  25488  ovolicc1  25502  iundisj  25534  volsup  25542  uniioombllem3  25571  vitalilem2  25595  vitalilem3  25596  mbfsup  25650  mbfinf  25651  mbflimsup  25652  itg2monolem1  25736  limcflflem  25866  limccnp  25877  limccnp2  25878  dvidlem  25901  dvn2bss  25916  cpnres  25923  dvcobr  25932  dvrec  25941  c1liplem1  25982  dvcnvrelem2  26004  dvfsumrlimf  26011  dvfsumlem1  26012  dvfsumlem2  26013  dvfsumlem3  26014  dvfsumlem4  26015  dvfsumrlim  26017  dvfsum2  26020  coeeulem  26208  coeid3  26224  plycn  26245  dvntaylp  26355  taylthlem1  26357  taylthlem2  26358  ulm2  26369  ulmshftlem  26373  ulmshft  26374  ulm0  26375  ulmcn  26383  ulmdvlem3  26386  ulmdv  26387  mtest  26388  mtestbdd  26389  dvradcnv  26405  psercn2  26407  psercn  26410  pserdv  26413  abelth  26425  efif1olem2  26526  efif1olem4  26528  efifo  26530  eff1olem  26531  logcn  26630  dvloglem  26631  cxpcn3  26731  resqrtcn  26732  sqrtcn  26733  logbleb  26766  logblt  26767  asinneg  26869  atanlogsub  26899  atanbnd  26909  ressatans  26917  leibpilem2  26924  xrlimcnp  26951  efrlim  26952  scvxcvx  26968  ppiub  27186  chtub  27194  logexprlim  27207  lgseisenlem1  27357  rplogsumlem1  27466  rplogsumlem2  27467  dchrisumlem2  27472  dchrisum0flb  27492  logdivbnd  27538  pntlem3  27591  dfnns2  28383  tgcgr4  28618  ltgov  28684  f1otrg  28958  eengtrkg  29074  iedgedg  29138  ushgredgedgloop  29319  subgruhgredgd  29372  uvtxupgrres  29496  umgr2v2evd2  29615  edginwlk  29722  wlk1walk  29726  crctcshwlkn0lem6  29902  wlkiswwlks1  29954  minvecolem1  30964  minvecolem2  30965  minvecolem4  30970  htthlem  31007  5oalem2  31745  3oalem2  31753  iundisjf  32679  fmptco1f1o  32726  xppreima  32738  xppreima2  32744  dfcnv2  32768  ccatws1f1o  33031  gsumhashmul  33149  xrge0tsmsd  33155  gsumwrd2dccatlem  33159  odpmco  33168  pmtrcnelor  33173  fzo0pmtrlast  33174  wrdpmtrlast  33175  pmtrto1cl  33181  psgnfzto1stlem  33182  fzto1stfv1  33183  fzto1st  33185  fzto1stinvn  33186  psgnfzto1st  33187  tocycf  33199  cycpmco2lem7  33214  cycpmco2  33215  cycpmrn  33225  cyc3evpm  33232  cyc3genpmlem  33233  cycpmgcl  33235  cyc3conja  33239  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspnsubrunlem1  33329  nsgmgc  33496  nsgqusf1olem1  33497  nsgqusf1olem2  33498  rhmpreimaprmidl  33535  ssdifidllem  33540  ssdifidl  33541  ssmxidllem  33557  drngmxidlr  33562  opprqus1r  33576  qsdrngilem  33578  qsdrngi  33579  rsprprmprmidlb  33615  rprmirredb  33624  1arithufdlem1  33636  1arithufdlem2  33637  1arithufdlem3  33638  1arithufdlem4  33639  fply1  33650  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  mplmulmvr  33732  psrmon  33742  psrmonprod  33745  esplylem  33759  esplyfv1  33762  esplysply  33764  esplyind  33768  ply1degltdimlem  33815  ply1degltdim  33816  algextdeglem4  33913  algextdeglem6  33915  algextdeglem7  33916  algextdeglem8  33917  nn0constr  33954  smatlem  33990  smatcl  33995  zartopn  34068  zarmxt1  34073  tpr2rico  34105  xrmulc1cn  34123  xrge0mulc1cn  34134  esumpfinvallem  34267  ldgenpisyslem1  34356  dynkin  34360  brfae  34441  sxbrsigalem3  34465  dya2icoseg2  34471  omsmeas  34516  sibfof  34533  sseqmw  34584  sseqf  34585  sseqp1  34588  fiblem  34591  fibp1  34594  probfinmeasbALTV  34622  repr0  34804  reprpmtf1o  34819  hgt750lemg  34847  bnj1379  35021  srcmpltd  35271  fineqvnttrclselem3  35313  subfacp1lem5  35421  subfacp1lem6  35422  cvxpconn  35479  cvxsconn  35480  cvmliftlem6  35527  cvmliftlem8  35529  cvmliftlem10  35531  cvmlift2lem6  35545  cvmlift2lem11  35550  cvmlift2lem12  35551  2goelgoanfmla1  35661  prv1n  35668  msubff  35767  msubco  35768  elmsta  35785  msubff1  35793  mvhf  35795  msubvrs  35797  iprodefisumlem  35977  filnetlem3  36617  ttcid  36729  ttcwf  36761  knoppcnlem10  36817  knoppcnlem11  36818  icoreunrn  37730  icoreelrn  37732  ralssiun  37778  poimirlem3  37999  poimirlem16  38012  poimirlem17  38013  poimirlem19  38015  poimirlem30  38026  dvasin  38080  cover2  38091  upixp  38105  sdclem1  38119  fdc  38121  caushft  38137  ismtyres  38184  rrncmslem  38208  isfld2  38381  presuc  38874  osumcllem10N  40466  pexmidlem7N  40477  dihglblem2N  41795  lcfrvalsnN  42042  lcfrlem5  42047  lcfrlem6  42048  lcfrlem27  42070  lcfrlem37  42080  aks6d1c1p4  42605  aks6d1c1p7  42607  aks6d1c1p8  42609  evl1gprodd  42611  aks6d1c2lem4  42621  aks6d1c5lem3  42631  aks6d1c6lem2  42665  prjspvs  43069  0prjspnrel  43086  monotuz  43395  expdiophlem1  43475  kelac2  43519  naddwordnexlem4  43855  grurankcld  44686  dvgrat  44765  nzss  44770  uzmptshftfval  44799  binomcxplemnotnn0  44809  orbitinit  45409  orbitcl  45410  permaxinf2lem  45465  refsumcn  45487  rfcnpre2  45488  rfcnpre3  45490  rfcnpre4  45491  disjf1o  45646  unirnmap  45661  unirnmapsn  45667  ssmapsn  45669  mptssid  45693  allbutfi  45845  eluzd  45860  uzidd2  45867  ressiocsup  46007  ressioosup  46008  ressiooinf  46010  fsumsermpt  46032  climexp  46058  climinf  46059  climsuse  46061  sumnnodd  46083  limsupresico  46151  limsupubuzlem  46163  limsupresxr  46217  liminfresxr  46218  liminfresico  46222  limsup10exlem  46223  cnrefiisplem  46280  cncfiooicclem1  46344  dvsinax  46364  itgsinexplem1  46405  fvvolioof  46440  fvvolicof  46442  stoweidlem14  46465  stoweidlem16  46467  stoweidlem31  46482  stoweidlem34  46485  stoweidlem36  46487  stoweidlem43  46494  stoweidlem46  46497  stoweidlem47  46498  stoweidlem52  46503  stoweidlem55  46506  stoweidlem57  46508  dirkercncf  46558  fourierdlem20  46578  fourierdlem42  46600  fourierdlem48  46605  fourierdlem49  46606  fourierdlem51  46608  fourierdlem54  46611  fourierdlem62  46619  fourierdlem71  46628  fourierdlem80  46637  fourierdlem114  46671  fouriersw  46682  ioorrnopnlem  46755  ioorrnopnxrlem  46757  salexct3  46793  salgencntex  46794  salgensscntex  46795  subsalsal  46810  sge0fodjrnlem  46867  sge0isum  46878  sge0seq  46897  sge0reuz  46898  sge0reuzb  46899  meadjiunlem  46916  meaiininclem  46937  carageniuncllem1  46972  caratheodorylem1  46977  hoiprodp1  47039  hoidmv1lelem1  47042  hoidmv1lelem2  47043  hoidmv1le  47045  hoidmvlelem1  47046  hoidmvlelem2  47047  hoidmvlelem3  47048  voncmpl  47072  hoiqssbl  47076  smflimlem2  47223  smfsuplem1  47262  smfsuplem3  47264  fsupdm  47293  finfdm  47297  cfsetsnfsetf  47529  fcores  47538  afvres  47643  afv2res  47710  fundcmpsurinjimaid  47894  iccpartigtl  47906  sprsymrelf  47978  prproropf1olem2  47987  uhgrimedgi  48389  isuspgrim0lem  48392  isuspgrimlem  48394  ushggricedg  48426  grimedg  48434  usgrgrtrirex  48449  isubgr3stgrlem7  48471  uspgrlimlem4  48490  grlimprclnbgr  48495  gpgiedgdmellem  48545  gpg3kgrtriex  48588  funcringcsetcALTV2lem3  48791  funcringcsetclem3ALTV  48814  lindslinindsimp2lem5  48961  rrxsphere  49247  line2  49251  iooii  49416  icccldii  49417  iscnrm3rlem3  49440  eloppf2  49632  oppcup  49705  natoppf  49727  zeroo2  49732  oppfdiag1  49912  oppfdiag  49914  2arwcat  50098  incat  50099  lmddu  50165  onsetreclem3  50205  amgmwlem  50300