Theorem eqeltri 2834

Description: Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
eqeltri.1	⊢ 𝐴 = 𝐵
eqeltri.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
eqeltri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltri.2	. 2 ⊢ 𝐵 ∈ 𝐶
2		eqeltri.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	eleq1i 2829	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
4	1, 3	mpbir 231	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  eqeltrri  2835  3eltr4i  2851  intab  4982  axrep6g  5295  unisn2  5317  inex2  5323  vpwex  5382  ord3ex  5392  zfpair  5426  vsnex  5439  opex  5474  otex  5475  uniopel  5525  elvvuni  5764  isarep2  6658  fvex  6919  fvexi  6920  riotaex  7391  ovexi  7464  tpex  7764  oprabex  7999  oprabrexex2  8001  mpoexw  8101  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  tfrlem16  8431  1oex  8514  2oex  8515  1on  8516  1onOLD  8517  2on  8518  2onOLD  8519  3on  8522  4on  8523  oesuclem  8561  oecl  8573  o2p2e4  8577  nnecl  8649  1onnALT  8677  2onnALT  8679  3onn  8680  4onn  8681  mapsnf1o2  8932  sbthlem10  9130  cnvfi  9214  fnfi  9215  nnunifi  9324  imafiOLD  9351  pwfi  9354  xpfiOLD  9356  prfiALT  9361  tpfi  9362  fczfsuppd  9423  cantnfvalf  9702  oemapwe  9731  cantnffval2  9732  cnfcom3clem  9742  ssttrcl  9752  r1fin  9810  hta  9934  infxpenlem  10050  alephon  10106  alephfplem1  10141  dfac5lem4  10163  dfac5lem5  10164  dfac5lem4OLD  10165  kmlem10  10197  fin1a2lem10  10446  fin1a2lem12  10448  hsmexlem9  10462  axcc2lem  10473  domtriomlem  10479  axdc2lem  10485  axcclem  10494  brdom7disj  10568  brdom6disj  10569  iundom2g  10577  konigthlem  10605  canthwelem  10687  wunex2  10775  wunex3  10778  1nq  10965  1pr  11052  nrex1  11101  axcnex  11184  ax1cn  11186  pnfex  11311  mnfxr  11315  inelr  12253  cju  12259  nnexALT  12265  2nn  12336  2re  12337  2cn  12338  3nn  12342  3re  12343  3cn  12344  4nn  12346  4re  12347  4cn  12348  5nn  12349  5re  12350  5cn  12351  6nn  12352  6re  12353  6cn  12354  7nn  12355  7re  12356  7cn  12357  8nn  12358  8re  12359  8cn  12360  9nn  12361  9re  12362  9cn  12363  nn0ex  12529  zexALT  12630  nneo  12699  zeo  12701  deccl  12745  10re  12749  decnncl  12750  numnncl2  12753  decnncl2  12754  numsucc  12770  numma2c  12776  numadd  12777  numaddc  12778  nummul1c  12779  nummul2c  12780  decmul1  12794  qexALT  13003  xrex  13026  xnegex  13246  xnegcl  13251  ixxssxr  13395  fz0to4untppr  13666  fz0to5un2tp  13667  om2uzuzi  13986  ltweuz  13998  axdc4uzlem  14020  seqex  14040  seqexw  14054  m1expcl2  14122  faccl  14318  facwordi  14324  faclbnd2  14326  bccl  14357  hashen1  14405  hashrabrsn  14407  hashunlei  14460  hashpw  14471  tpf1o  14536  s1cli  14639  ccat2s1p1  14663  cats1un  14755  revs1  14799  cshwsexa  14858  cshwsexaOLD  14859  cats1cli  14892  cats1fvn  14893  crre  15149  remim  15152  climmpt  15603  sumex  15720  supcvg  15888  geo2lim  15907  prodex  15937  bpoly4  16091  ere  16121  eftlub  16141  efsep  16142  tan0  16183  ef01bndlem  16216  nn0o  16416  divalglem5  16430  divalglem9  16434  sadcf  16486  smupf  16511  crth  16811  phimullem  16812  pczpre  16880  pockthi  16940  prmreclem2  16950  igz  16967  0ramcl  17056  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  4001prm  17178  strle1  17191  ndxarg  17229  basendxnn  17254  basendxnnOLD  17255  plusgndxnn  17325  tsetndxnn  17399  plendxnn  17413  dsndxnn  17432  unifndxnn  17442  prdsbasex  17496  prdsds  17510  yonedalem3  18336  isposix  18382  isposixOLD  18383  plusffval  18671  issubmgm2  18728  efmnd1hash  18917  efmnd2hash  18919  smndex1bas  18931  smndex1sgrp  18933  smndex1mnd  18935  smndex1id  18936  smndex2dbas  18939  smndex2hbas  18941  grpsubfval  19013  mulgfval  19099  symg1hash  19421  symg2hash  19423  symgvalstruct  19428  symgvalstructOLD  19429  symgfisg  19500  psgnsn  19552  psgnprfval1  19554  odfval  19564  sylow2alem2  19650  efgsval2  19765  efgsp1  19769  pgpfaclem1  20115  dvdsrval  20377  isirred  20435  scaffval  20894  cnfldex  21384  xrsex  21412  pzriprnglem4  21512  pzriprnglem5  21513  pzriprnglem6  21514  pzriprng1ALT  21524  zlmlemOLD  21545  znle  21568  znidomb  21597  cnmsgnsubg  21612  refld  21654  ipffval  21683  psrbag0  22103  psrbagsn  22104  psr1baslem  22201  mat1dimbas  22493  mat1dimscm  22496  mat1f1o  22499  mat1rhmelval  22501  m2detleib  22652  pmatcoe1fsupp  22722  indistopon  23023  iccordt  23237  conncompid  23454  ptbasfi  23604  ptcmpfi  23836  ustfn  24225  ust0  24243  ustn0  24244  tmslem  24509  tmslemOLD  24510  nmfval  24616  tnglemOLD  24669  cnbl0  24809  cnopn  24822  remet  24825  re2ndc  24836  zcld  24848  icccmp  24860  xrge0gsumle  24868  xrge0tsms  24869  xmetdcn  24873  divcnOLD  24903  divcn  24905  expcn  24909  expcnOLD  24911  iiconn  24926  idcncf  24957  cnmpopc  24968  cnrehmeo  24997  cnrehmeoOLD  24998  cnheiborlem  24999  rellycmp  25002  bndth  25003  evth2  25005  cnrlmod  25189  cnrlvec  25190  cncmet  25369  ishl2  25417  ehleudis  25465  ehleudisval  25466  finiunmbl  25592  ioombl1lem4  25609  vitalilem4  25659  vitalilem5  25660  ismbf2d  25688  mbfimaopnlem  25703  mbfi1fseqlem6  25769  itgex  25819  bddmulibl  25888  ditgex  25901  recnperf  25954  dvcnvrelem2  26071  ftc1  26097  mdegcl  26122  plyeq0lem  26263  aaliou3lem4  26402  dvradcnv  26478  sincn  26502  coscn  26503  tanabsge  26562  circsubm  26609  reloggim  26655  logcn  26703  dvloglem  26704  logdmopn  26705  dvlog2  26709  2irrexpq  26787  cxpcn  26801  cxpcnOLD  26802  cxpcn3  26805  resqrtcn  26806  2logb9irrALT  26855  2irrexpqALT  26857  atanrecl  26968  atan1  26985  atansopn  26989  birthdaylem1  27008  birthday  27011  emcllem4  27056  emcllem6  27058  lgamgulmlem6  27091  basellem6  27143  ppiublem1  27260  bposlem6  27347  bposlem8  27349  lgslem4  27358  lgsdir2lem2  27384  selberglem1  27603  selberglem3  27605  selberg  27606  selbergs  27632  qdrng  27678  0sno  27885  1sno  27886  lrrecse  27989  precsexlem11  28255  seqsex  28305  nnsex  28337  n0sbday  28368  n0subs  28374  n0p1nns  28375  dfnns2  28376  zsex  28380  zs12ex  28436  edgfndxnn  29021  structvtxvallem  29051  usgrexmpllem  29291  usgrexmpl  29294  uhgrspan1  29334  upgrres  29337  umgrres  29338  usgrres  29339  upgrres1  29344  umgrres1  29345  usgrres1  29346  fusgrfis  29361  cusgrres  29480  vtxdlfgrval  29517  vtxdusgr0edgnelALT  29528  umgr2v2e  29557  vtxdginducedm1lem1  29571  vtxdginducedm1fi  29576  finsumvtxdg2ssteplem4  29580  pthdlem1  29798  crctcshlem3  29848  2wlkd  29965  2wlkond  29966  2trlond  29968  2pthd  29969  2pthond  29971  umgr2adedgwlkonALT  29976  0pth  30153  wlk2v2e  30185  3wlkd  30198  3trlond  30201  3pthd  30202  3pthond  30203  3spthond  30205  eupthvdres  30263  eulerpathpr  30268  konigsbergumgr  30279  konigsberglem5  30284  konigsberg  30285  ex-lcm  30486  isvciOLD  30608  isnvi  30641  blocni  30833  hmoval  30838  cncph  30847  ipasslem7  30864  siilem2  30880  normlem2  31139  normlem3  31140  normlem6  31143  h0elch  31283  hhssabloilem  31289  hhsssh  31297  spansnji  31674  nonbooli  31679  3oalem5  31694  3oalem6  31695  3oai  31696  mayetes3i  31757  nmcexi  32054  nmbdfnlb  32078  rnelshi  32087  cnlnadjlem5  32099  pjbdlni  32177  golem2  32300  goeqi  32301  dp2clq  32847  rpdp2cl  32848  rpdp2cl2  32849  dpmul100  32863  rpdpcl  32869  chnub  32985  xrge0tsmsd  33047  pmtrto1cl  33101  psgnfzto1stlem  33102  fzto1st  33105  psgnfzto1st  33107  nn0omnd  33352  xrge0slmod  33355  qusima  33415  prmidl0  33457  fply1  33563  ply1degltdimlem  33649  ccfldextdgrr  33696  algextdeglem8  33729  constrfin  33750  2sqr3minply  33752  circtopn  33797  circcn  33798  zarcmplem  33841  tpr2tp  33864  tpr2rico  33872  ordtprsval  33878  ordtprsuni  33879  ordtrestNEW  33881  ordtrest2NEWlem  33882  ordtrest2NEW  33883  ordtconnlem1  33884  mndpluscn  33886  xrge0pluscn  33900  xrge0mulc1cn  33901  xrge0haus  33904  lmlimxrge0  33908  lmxrge0  33912  qqhcn  33953  qqhucn  33954  esumex  34009  esumcst  34043  hasheuni  34065  esumcvg  34066  prsiga  34111  brsiga  34163  mbfmcnt  34249  sxbrsigalem3  34253  dya2iocuni  34264  dya2iocucvr  34265  sxbrsigalem1  34266  sxbrsiga  34271  eulerpartlemt  34352  fibp1  34382  coinflipprob  34460  coinfliprv  34463  ccatmulgnn0dir  34535  signswplusg  34548  hgt750lem2  34645  hgt750leme  34651  bnj105  34716  bnj918  34758  bnj95  34856  bnj852  34913  bnj865  34915  subfacp1lem1  35163  subfacp1lem3  35166  subfacp1lem5  35168  subfacp1lem6  35169  kur14lem7  35196  iisconn  35236  iillysconn  35237  cvmliftlem5  35273  cvmliftlem8  35276  cvmliftlem10  35278  cvmlift2lem9  35295  satfv0  35342  goalrlem  35380  goalr  35381  satffunlem2lem2  35390  circum  35658  iexpire  35714  altopex  35941  colinearex  36041  ssoninhaus  36430  cnndvlem2  36520  bj-prex  37022  bj-prfromadj  37027  bj-pinftyccb  37203  taupi  37305  isbasisrelowl  37340  relowlpssretop  37346  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  dvasin  37690  dvacos  37691  areacirc  37699  upixp  37715  fdc  37731  lmclim2  37744  cncfres  37751  heibor1lem  37795  rrnval  37813  rrnmet  37815  reheibor  37825  isdrngo2  37944  isrngohom  37951  idlval  37999  isidl  38000  igenval  38047  scottexf  38154  cnvepresex  38315  renegclALT  38944  ldualfvadd  39109  cmtfvalN  39191  cvrfval  39249  cdleme31fv  40372  cdlemk40  40899  cdlemk56  40953  dibopelvalN  41125  dibopelval2  41127  dibelval3  41129  diblsmopel  41153  cdlemn11a  41189  dihopelvalcpre  41230  dihpN  41318  hlhilsca  41917  hlhilip  41934  3factsumint1  42002  lcmineqlem23  42032  aks4d1p1p6  42054  aks4d1p1p5  42056  aks6d1c6isolem2  42156  itrere  42331  acos1half  42366  redvmptabs  42368  readvrec2  42369  sn-0tie0  42445  sn-itrere  42474  sn-retire  42475  prjspval  42589  flt4lem5e  42642  sn-isghm  42659  mapfzcons2  42706  jm2.23  42984  jm2.27dlem2  42998  jm2.27dlem4  43000  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  expdioph  43011  aomclem6  43047  pwslnmlem0  43079  frlmpwfi  43086  mncn0  43127  aaitgo  43150  arearect  43203  areaquad  43204  omcl3g  43323  comptiunov2i  43695  frege110  43962  frege133  43985  scottex2  44240  radcnvrat  44309  uzmptshftfval  44341  dvradcnv2  44342  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemnotnn0  44351  rfcnpre1  44956  fcnre  44962  refsumcn  44967  refsum2cnlem1  44974  unirnmapsn  45156  infxrpnf  45395  iocopn  45472  icoopn  45477  mccl  45553  clim1fr1  45556  islptre  45574  sumnnodd  45585  lptre2pt  45595  limclner  45606  limclr  45610  expfac  45612  0cnf  45832  icccncfext  45842  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  itgsin0pilem1  45905  iblempty  45920  itgvol0  45923  stoweidlem47  46002  stoweidlem53  46008  stoweidlem57  46012  stoweidlem59  46014  wallispilem3  46022  wallispilem4  46023  wallispilem5  46024  wallispi  46025  stirlinglem1  46029  stirlinglem8  46036  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  dirkerper  46051  dirkercncflem2  46059  fourierdlem16  46078  fourierdlem21  46083  fourierdlem22  46084  fourierdlem36  46098  fourierdlem42  46104  fourierdlem71  46132  fourierdlem83  46144  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem114  46175  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  etransclem48  46237  salexct3  46297  salgencntex  46298  salgensscntex  46299  iooborel  46306  bor1sal  46310  gsumge0cl  46326  sge0tsms  46335  sge0isum  46382  nnfoctbdjlem  46410  isomenndlem  46485  mbfresmf  46694  incsmflem  46696  incsmf  46697  smfmbfcex  46715  decsmflem  46721  decsmf  46722  smflimlem1  46726  smfpimbor1lem2  46754  smf2id  46756  smfco  46757  smfpimcclem  46762  tworepnotupword  46839  sprsymrelfolem1  47416  sprbisymrel  47423  fmtno0prm  47482  fmtno1prm  47483  fmtno2prm  47484  fmtno3prm  47486  fmtno4prm  47499  m2prm  47515  m3prm  47516  m5prm  47522  m7prm  47524  lighneallem4a  47532  0evenALTV  47612  1oddALTV  47614  2evenALTV  47616  6even  47635  7odd  47636  8even  47637  9gbo  47698  opstrgric  47832  ushggricedg  47833  grtri  47844  usgrexmpl1  47916  usgrexmpl1vtx  47917  usgrexmpl1edg  47918  usgrexmpl2  47921  usgrexmpl2vtx  47922  usgrexmpl2edg  47923  uspgrex  47993  lmod1zrnlvec  48339  zlmodzxzldeplem1  48345  zlmodzxzldeplem3  48347  zlmodzxzldeplem4  48348  zlmodzxzldep  48349  ldepsnlinclem1  48350  ldepsnlinclem2  48351  blennn0elnn  48426  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  itcovalpclem2  48520  itcovalt2lem2  48525  ackval42  48545  rrx2line  48589  rrx2linesl  48592  spheres  48595  2sphere  48598  2sphere0  48599  line2x  48603  line2y  48604  functhinclem1  48840  prsthinc  48854