Theorem eleqtrrdi 2848

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  3eltr4g  2854  brelrng  5898  elabrex  7198  elabrexg  7199  fliftel1  7266  ovidig  7510  unielxp  7981  tfrlem11  8329  rdglim  8367  seqomlem4  8394  2oconcl  8440  ecopqsi  8719  erov  8763  eroprf  8764  sbthlem2  9028  dffi3  9346  ixpiunwdom  9507  cantnfcl  9588  r1lim  9696  rankwflemb  9717  pwwf  9731  unwf  9734  rankwflem  9739  uniwf  9743  rankpwi  9747  rankr1g  9756  r1pw  9769  r1rankid  9783  rankuni  9787  djulcl  9834  djurcl  9835  inlresf  9838  inrresf  9840  djuun  9850  cardlim  9896  infxpenlem  9935  alephfp  10030  cfsmolem  10192  alephsing  10198  hsmexlem4  10351  axdc3lem2  10373  numth3  10392  iunfo  10461  konigthlem  10491  iunctb  10497  canthwelem  10573  canthwe  10574  r1limwun  10659  inar1  10698  inatsk  10701  gruina  10741  grur1  10743  tskmval  10762  tskmcl  10764  pinq  10850  dmrecnq  10891  addclsr  11006  mulclsr  11007  axaddf  11068  axmulf  11069  peano2nn  12169  uztrn2  12782  eluz2nn  12813  peano2uzs  12827  uzsupss  12865  uzsup  13795  uzrdgfni  13893  uzrdgsuci  13895  fsuppmapnn0fiub  13926  seqf  13958  ser0  13989  bcm1k  14250  bcp1nk  14252  bcpasc  14256  hashprdifel  14333  fz1isolem  14396  pr2pwpr  14414  tpf  14434  ccats1val2  14563  rexuzre  15288  limsupgre  15416  climconst  15478  rlimclim1  15480  climrlim2  15482  clim2ser  15590  clim2ser2  15591  iserex  15592  isermulc2  15593  iserle  15595  isercolllem3  15602  isercoll2  15604  climsup  15605  iseraltlem2  15618  iseraltlem3  15619  zsum  15653  isumclim3  15694  isumadd  15702  fsump1i  15704  iserabs  15750  cvgcmp  15751  cvgcmpub  15752  cvgcmpce  15753  abscvgcvg  15754  isumshft  15774  isumsplit  15775  isum1p  15776  isumrpcl  15778  isumsup2  15781  climcndslem1  15784  cvgrat  15818  clim2prod  15823  clim2div  15824  prodf1  15826  ntrivcvgn0  15833  ntrivcvgtail  15835  fprodntriv  15877  fprodabs  15909  fprodeq0  15910  iprodclim3  15935  iprodmul  15938  ef0lem  16013  fprodefsum  16030  rpnnen2lem3  16153  dvdsflip  16256  fzo0dvdseq  16262  bitsinv1  16381  smupval  16427  smueqlem  16429  seq1st  16510  algr0  16511  prmind2  16624  crth  16717  eulerthlem2  16721  prmdiv  16724  pockthlem  16845  pockthg  16846  unbenlem  16848  prmunb  16854  prmgaplem7  16997  strfv2d  17140  imasvscaval  17471  oppccatid  17654  oppccatf  17663  epii  17679  fthepi  17866  funcestrcsetclem3  18077  funcsetcestrclem3  18091  yon12  18200  yon2  18201  yonedalem4c  18212  yonedalem22  18213  yonedalem3b  18214  yonedainv  18216  acsmapd  18489  chnub  18557  chnccats1  18560  chnccat  18561  mgm2nsgrplem1  18858  mgm2nsgrplem2  18859  mgm2nsgrplem3  18860  sgrp2nmndlem1  18863  sgrp2rid2  18866  ghmqusker  19231  cntrsubgnsg  19287  symgpssefmnd  19340  pmtrrn  19401  gexcl3  19531  efgi  19663  efgi2  19669  efgs1b  19680  efgredlemg  19686  efgredlemd  19688  frgpnabllem1  19817  cycsubgcyg  19845  gsumzaddlem  19865  dprdwd  19957  dprd2da  19988  rhmopp  20457  lsppratlem3  21119  lsppratlem4  21120  lbsextlem2  21129  lidl0ALT  21198  lidl1ALT  21201  2idl0  21230  2idl1  21231  domnchr  21502  znf1o  21521  mplsubrglem  21974  mpfconst  22079  mpfproj  22080  mpfind  22085  mhpmulcl  22107  pf1const  22305  pf1id  22306  mpfpf1  22310  pf1mpf  22311  madetsumid  22420  slesolex  22641  pmatcoe1fsupp  22660  mat2pmatbas0  22686  pmatcollpw  22740  pm2mpf1  22758  isclo  23046  indiscld  23050  restntr  23141  ordtbaslem  23147  ordtbas2  23150  lmconst  23220  lmss  23257  conncompid  23390  2ndcomap  23417  locfincmp  23485  comppfsc  23491  xkouni  23558  txcls  23563  ptclsg  23574  uptx  23584  txindis  23593  tx1stc  23609  cnmpt1res  23635  tgqtop  23671  uffix  23880  cnpflf2  23959  ptcmplem2  24012  ptcmplem4  24014  tgpconncomp  24072  tsmsfbas  24087  fmucnd  24250  prdsxmetlem  24327  imasdsf1olem  24332  prdsbl  24450  blcvx  24757  xrsmopn  24772  xrge0tsms  24794  metdcn2  24799  expcncf  24891  cnmpopc  24893  icchmeo  24909  icchmeoOLD  24910  iccpnfhmeo  24914  cnheibor  24925  evth  24929  evth2  24930  lebnumlem2  24932  lebnumii  24936  reparphti  24967  reparphtiOLD  24968  cfilfcls  25245  minveclem2  25397  minveclem3  25400  minveclem4  25403  ovoliunlem1  25474  ovolicc1  25488  iundisj  25520  volsup  25528  uniioombllem3  25557  vitalilem2  25581  vitalilem3  25582  mbfsup  25636  mbfinf  25637  mbflimsup  25638  itg2monolem1  25722  limcflflem  25852  limccnp  25863  limccnp2  25864  dvidlem  25887  dvn2bss  25903  cpnres  25910  dvcobr  25920  dvcobrOLD  25921  dvrec  25930  c1liplem1  25972  dvcnvrelem2  25994  dvfsumrlimf  26002  dvfsumlem1  26003  dvfsumlem2  26004  dvfsumlem2OLD  26005  dvfsumlem3  26006  dvfsumlem4  26007  dvfsumrlim  26009  dvfsum2  26012  coeeulem  26200  coeid3  26216  plycn  26237  plycnOLD  26238  dvntaylp  26350  taylthlem1  26352  taylthlem2  26353  taylthlem2OLD  26354  ulm2  26365  ulmshftlem  26369  ulmshft  26370  ulm0  26371  ulmcn  26379  ulmdvlem3  26382  ulmdv  26383  mtest  26384  mtestbdd  26385  dvradcnv  26401  psercn2  26403  psercn2OLD  26404  psercn  26407  pserdv  26410  abelth  26422  efif1olem2  26523  efif1olem4  26525  efifo  26527  eff1olem  26528  logcn  26627  dvloglem  26628  cxpcn3  26729  resqrtcn  26730  sqrtcn  26731  logbleb  26764  logblt  26765  asinneg  26867  atanlogsub  26897  atanbnd  26907  ressatans  26915  leibpilem2  26922  xrlimcnp  26949  efrlim  26950  efrlimOLD  26951  scvxcvx  26967  ppiub  27186  chtub  27194  logexprlim  27207  lgseisenlem1  27357  rplogsumlem1  27466  rplogsumlem2  27467  dchrisumlem2  27472  dchrisum0flb  27492  logdivbnd  27538  pntlem3  27591  dfnns2  28383  tgcgr4  28619  ltgov  28685  f1otrg  28959  eengtrkg  29075  iedgedg  29139  ushgredgedgloop  29320  subgruhgredgd  29373  uvtxupgrres  29497  umgr2v2evd2  29617  edginwlk  29724  wlk1walk  29728  crctcshwlkn0lem6  29904  wlkiswwlks1  29956  minvecolem1  30966  minvecolem2  30967  minvecolem4  30972  htthlem  31009  5oalem2  31747  3oalem2  31755  iundisjf  32680  fmptco1f1o  32727  xppreima  32739  xppreima2  32745  dfcnv2  32769  ccatws1f1o  33048  gsumhashmul  33165  xrge0tsmsd  33171  gsumwrd2dccatlem  33175  odpmco  33184  pmtrcnelor  33189  fzo0pmtrlast  33190  wrdpmtrlast  33191  pmtrto1cl  33197  psgnfzto1stlem  33198  fzto1stfv1  33199  fzto1st  33201  fzto1stinvn  33202  psgnfzto1st  33203  tocycf  33215  cycpmco2lem7  33230  cycpmco2  33231  cycpmrn  33241  cyc3evpm  33248  cyc3genpmlem  33249  cycpmgcl  33251  cyc3conja  33255  elrgspnlem1  33340  elrgspnlem2  33341  elrgspnlem3  33342  elrgspnlem4  33343  elrgspnsubrunlem1  33345  nsgmgc  33509  nsgqusf1olem1  33510  nsgqusf1olem2  33511  rhmpreimaprmidl  33548  ssdifidllem  33553  ssdifidl  33554  ssmxidllem  33570  drngmxidlr  33575  opprqus1r  33589  qsdrngilem  33591  qsdrngi  33592  rsprprmprmidlb  33620  rprmirredb  33629  1arithufdlem1  33641  1arithufdlem2  33642  1arithufdlem3  33643  1arithufdlem4  33644  fply1  33655  ply1degltel  33691  ply1degleel  33692  ply1degltlss  33693  mplmulmvr  33720  psrmon  33730  psrmonprod  33733  esplylem  33747  esplyfv1  33750  esplysply  33752  esplyind  33756  ply1degltdimlem  33804  ply1degltdim  33805  algextdeglem4  33902  algextdeglem6  33904  algextdeglem7  33905  algextdeglem8  33906  nn0constr  33943  smatlem  33979  smatcl  33984  zartopn  34057  zarmxt1  34062  tpr2rico  34094  xrmulc1cn  34112  xrge0mulc1cn  34123  esumpfinvallem  34256  ldgenpisyslem1  34345  dynkin  34349  brfae  34430  sxbrsigalem3  34454  dya2icoseg2  34460  omsmeas  34505  sibfof  34522  sseqmw  34573  sseqf  34574  sseqp1  34577  fiblem  34580  fibp1  34583  probfinmeasbALTV  34611  repr0  34793  reprpmtf1o  34808  hgt750lemg  34836  bnj1379  35010  srcmpltd  35260  fineqvnttrclselem3  35305  subfacp1lem5  35404  subfacp1lem6  35405  cvxpconn  35462  cvxsconn  35463  cvmliftlem6  35510  cvmliftlem8  35512  cvmliftlem10  35514  cvmlift2lem6  35528  cvmlift2lem11  35533  cvmlift2lem12  35534  2goelgoanfmla1  35644  prv1n  35651  msubff  35750  msubco  35751  elmsta  35768  msubff1  35776  mvhf  35778  msubvrs  35780  iprodefisumlem  35960  filnetlem3  36600  knoppcnlem10  36728  knoppcnlem11  36729  icoreunrn  37618  icoreelrn  37620  ralssiun  37666  poimirlem3  37878  poimirlem16  37891  poimirlem17  37892  poimirlem19  37894  poimirlem30  37905  dvasin  37959  cover2  37970  upixp  37984  sdclem1  37998  fdc  38000  caushft  38016  ismtyres  38063  rrncmslem  38087  isfld2  38260  presuc  38753  osumcllem10N  40345  pexmidlem7N  40356  dihglblem2N  41674  lcfrvalsnN  41921  lcfrlem5  41926  lcfrlem6  41927  lcfrlem27  41949  lcfrlem37  41959  aks6d1c1p4  42485  aks6d1c1p7  42487  aks6d1c1p8  42489  evl1gprodd  42491  aks6d1c2lem4  42501  aks6d1c5lem3  42511  aks6d1c6lem2  42545  prjspvs  42972  0prjspnrel  42989  monotuz  43302  expdiophlem1  43382  kelac2  43426  naddwordnexlem4  43762  grurankcld  44593  dvgrat  44672  nzss  44677  uzmptshftfval  44706  binomcxplemnotnn0  44716  orbitinit  45316  orbitcl  45317  permaxinf2lem  45372  refsumcn  45394  rfcnpre2  45395  rfcnpre3  45397  rfcnpre4  45398  disjf1o  45554  unirnmap  45570  unirnmapsn  45576  ssmapsn  45578  mptssid  45603  allbutfi  45755  eluzd  45771  uzidd2  45778  ressiocsup  45918  ressioosup  45919  ressiooinf  45921  fsumsermpt  45943  climexp  45969  climinf  45970  climsuse  45972  sumnnodd  45994  limsupresico  46062  limsupubuzlem  46074  limsupresxr  46128  liminfresxr  46129  liminfresico  46133  limsup10exlem  46134  cnrefiisplem  46191  cncfiooicclem1  46255  dvsinax  46275  itgsinexplem1  46316  fvvolioof  46351  fvvolicof  46353  stoweidlem14  46376  stoweidlem16  46378  stoweidlem31  46393  stoweidlem34  46396  stoweidlem36  46398  stoweidlem43  46405  stoweidlem46  46408  stoweidlem47  46409  stoweidlem52  46414  stoweidlem55  46417  stoweidlem57  46419  dirkercncf  46469  fourierdlem20  46489  fourierdlem42  46511  fourierdlem48  46516  fourierdlem49  46517  fourierdlem51  46519  fourierdlem54  46522  fourierdlem62  46530  fourierdlem71  46539  fourierdlem80  46548  fourierdlem114  46582  fouriersw  46593  ioorrnopnlem  46666  ioorrnopnxrlem  46668  salexct3  46704  salgencntex  46705  salgensscntex  46706  subsalsal  46721  sge0fodjrnlem  46778  sge0isum  46789  sge0seq  46808  sge0reuz  46809  sge0reuzb  46810  meadjiunlem  46827  meaiininclem  46848  carageniuncllem1  46883  caratheodorylem1  46888  hoiprodp1  46950  hoidmv1lelem1  46953  hoidmv1lelem2  46954  hoidmv1le  46956  hoidmvlelem1  46957  hoidmvlelem2  46958  hoidmvlelem3  46959  voncmpl  46983  hoiqssbl  46987  smflimlem2  47134  smfsuplem1  47173  smfsuplem3  47175  fsupdm  47204  finfdm  47208  cfsetsnfsetf  47422  fcores  47431  afvres  47536  afv2res  47603  fundcmpsurinjimaid  47775  iccpartigtl  47787  sprsymrelf  47859  prproropf1olem2  47868  uhgrimedgi  48254  isuspgrim0lem  48257  isuspgrimlem  48259  ushggricedg  48291  grimedg  48299  usgrgrtrirex  48314  isubgr3stgrlem7  48336  uspgrlimlem4  48355  grlimprclnbgr  48360  gpgiedgdmellem  48410  gpg3kgrtriex  48453  funcringcsetcALTV2lem3  48656  funcringcsetclem3ALTV  48679  lindslinindsimp2lem5  48826  rrxsphere  49112  line2  49116  iooii  49281  icccldii  49282  iscnrm3rlem3  49305  eloppf2  49497  oppcup  49570  natoppf  49592  zeroo2  49597  oppfdiag1  49777  oppfdiag  49779  2arwcat  49963  incat  49964  lmddu  50030  onsetreclem3  50070  amgmwlem  50165