Theorem eqeltri 2827

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 2822	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
4	1, 3	mpbir 230	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1539   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808

This theorem is referenced by:  eqeltrri  2828  3eltr4i  2844  intab  4981  axrep6g  5292  unisn2  5311  inex2  5317  vpwex  5374  ord3ex  5384  zfpair  5418  vsnex  5428  opex  5463  otex  5464  uniopel  5515  elvvuni  5751  isarep2  6638  fvex  6903  fvexi  6904  riotaex  7371  ovexi  7445  tpex  7736  oprabex  7965  oprabrexex2  7967  mpoexw  8067  mptmpoopabbrd  8069  tfrlem16  8395  1oex  8478  2oex  8479  1on  8480  1onOLD  8481  2on  8482  2onOLD  8483  3on  8486  4on  8487  2oexOLD  8489  oesuclem  8527  oecl  8539  o2p2e4  8543  nnecl  8615  1onnALT  8642  2onnALT  8644  3onn  8645  4onn  8646  mapsnf1o2  8890  sbthlem10  9094  imafi  9177  pwfi  9180  cnvfi  9182  fnfi  9183  nnunifi  9296  xpfiOLD  9320  prfi  9324  tpfi  9325  pwfiOLD  9349  fczfsuppd  9383  cantnfvalf  9662  oemapwe  9691  cantnffval2  9692  cnfcom3clem  9702  ssttrcl  9712  r1fin  9770  hta  9894  infxpenlem  10010  alephon  10066  alephfplem1  10101  dfac5lem4  10123  dfac5lem5  10124  kmlem10  10156  fin1a2lem10  10406  fin1a2lem12  10408  hsmexlem9  10422  axcc2lem  10433  domtriomlem  10439  axdc2lem  10445  axcclem  10454  brdom7disj  10528  brdom6disj  10529  iundom2g  10537  konigthlem  10565  canthwelem  10647  wunex2  10735  wunex3  10738  1nq  10925  1pr  11012  nrex1  11061  axcnex  11144  ax1cn  11146  pnfex  11271  mnfxr  11275  inelr  12206  cju  12212  nnexALT  12218  2nn  12289  2re  12290  2cn  12291  3nn  12295  3re  12296  3cn  12297  4nn  12299  4re  12300  4cn  12301  5nn  12302  5re  12303  5cn  12304  6nn  12305  6re  12306  6cn  12307  7nn  12308  7re  12309  7cn  12310  8nn  12311  8re  12312  8cn  12313  9nn  12314  9re  12315  9cn  12316  nn0ex  12482  zexALT  12582  nneo  12650  zeo  12652  deccl  12696  10re  12700  decnncl  12701  numnncl2  12704  decnncl2  12705  numsucc  12721  numma2c  12727  numadd  12728  numaddc  12729  nummul1c  12730  nummul2c  12731  decmul1  12745  qexALT  12952  xrex  12975  xnegex  13191  xnegcl  13196  ixxssxr  13340  om2uzuzi  13918  ltweuz  13930  axdc4uzlem  13952  seqex  13972  seqexw  13986  m1expcl2  14055  faccl  14247  facwordi  14253  faclbnd2  14255  bccl  14286  hashen1  14334  hashrabrsn  14336  hashunlei  14389  hashpw  14400  s1cli  14559  ccat2s1p1  14583  cats1un  14675  revs1  14719  cshwsexa  14778  cshwsexaOLD  14779  cats1cli  14812  cats1fvn  14813  crre  15065  remim  15068  climmpt  15519  sumex  15638  supcvg  15806  geo2lim  15825  prodex  15855  bpoly4  16007  ere  16036  eftlub  16056  efsep  16057  tan0  16098  ef01bndlem  16131  nn0o  16330  divalglem5  16344  divalglem9  16348  sadcf  16398  smupf  16423  crth  16715  phimullem  16716  pczpre  16784  pockthi  16844  prmreclem2  16854  igz  16871  0ramcl  16960  1259lem1  17068  1259lem2  17069  1259lem3  17070  1259lem4  17071  1259lem5  17072  1259prm  17073  2503lem1  17074  2503lem2  17075  2503lem3  17076  2503prm  17077  4001lem1  17078  4001lem2  17079  4001lem3  17080  4001lem4  17081  4001prm  17082  strle1  17095  ndxarg  17133  basendxnn  17158  basendxnnOLD  17159  plusgndxnn  17229  tsetndxnn  17303  plendxnn  17317  dsndxnn  17336  unifndxnn  17346  prdsbasex  17400  prdsds  17414  yonedalem3  18237  isposix  18282  isposixOLD  18283  plusffval  18571  issubmgm2  18628  efmnd1hash  18809  efmnd2hash  18811  smndex1bas  18823  smndex1sgrp  18825  smndex1mnd  18827  smndex1id  18828  smndex2dbas  18831  smndex2hbas  18833  grpsubfval  18904  mulgfval  18988  symg1hash  19298  symg2hash  19300  symgvalstruct  19305  symgvalstructOLD  19306  symgfisg  19377  psgnsn  19429  psgnprfval1  19431  odfval  19441  sylow2alem2  19527  efgsval2  19642  efgsp1  19646  pgpfaclem1  19992  dvdsrval  20252  isirred  20310  scaffval  20634  xrsex  21160  pzriprnglem4  21253  pzriprnglem5  21254  pzriprnglem6  21255  pzriprng1ALT  21265  zlmlemOLD  21286  znle  21307  znidomb  21336  cnmsgnsubg  21349  refld  21391  ipffval  21420  psrbag0  21842  psrbagsn  21843  psr1baslem  21928  mat1dimbas  22194  mat1dimscm  22197  mat1f1o  22200  mat1rhmelval  22202  m2detleib  22353  pmatcoe1fsupp  22423  indistopon  22724  iccordt  22938  conncompid  23155  ptbasfi  23305  ptcmpfi  23537  ustfn  23926  ust0  23944  ustn0  23945  tmslem  24210  tmslemOLD  24211  nmfval  24317  tnglemOLD  24370  cnbl0  24510  cnopn  24523  remet  24526  re2ndc  24537  zcld  24549  icccmp  24561  xrge0gsumle  24569  xrge0tsms  24570  xmetdcn  24574  divcnOLD  24604  divcn  24606  expcn  24610  expcnOLD  24612  iiconn  24627  idcncf  24658  cnmpopc  24669  cnrehmeo  24698  cnrehmeoOLD  24699  cnheiborlem  24700  rellycmp  24703  bndth  24704  evth2  24706  cnrlmod  24890  cnrlvec  24891  cncmet  25070  ishl2  25118  ehleudis  25166  ehleudisval  25167  finiunmbl  25293  ioombl1lem4  25310  vitalilem4  25360  vitalilem5  25361  ismbf2d  25389  mbfimaopnlem  25404  mbfi1fseqlem6  25470  itgex  25520  bddmulibl  25588  ditgex  25601  recnperf  25654  dvcnvrelem2  25770  ftc1  25794  mdegcl  25822  plyeq0lem  25959  aaliou3lem4  26095  dvradcnv  26169  sincn  26192  coscn  26193  tanabsge  26252  circsubm  26298  reloggim  26343  logcn  26391  dvloglem  26392  logdmopn  26393  dvlog2  26397  2irrexpq  26475  cxpcn  26489  cxpcn3  26492  resqrtcn  26493  2logb9irrALT  26539  2irrexpqALT  26541  atanrecl  26652  atan1  26669  atansopn  26673  birthdaylem1  26692  birthday  26695  emcllem4  26739  emcllem6  26741  lgamgulmlem6  26774  basellem6  26826  ppiublem1  26941  bposlem6  27028  bposlem8  27030  lgslem4  27039  lgsdir2lem2  27065  selberglem1  27284  selberglem3  27286  selberg  27287  selbergs  27313  qdrng  27359  0sno  27564  1sno  27565  lrrecse  27664  precsexlem11  27902  n0sex  27933  nnsex  27934  edgfndxnn  28517  structvtxvallem  28547  usgrexmpllem  28784  usgrexmpl  28787  uhgrspan1  28827  upgrres  28830  umgrres  28831  usgrres  28832  upgrres1  28837  umgrres1  28838  usgrres1  28839  fusgrfis  28854  cusgrres  28972  vtxdlfgrval  29009  vtxdusgr0edgnelALT  29020  umgr2v2e  29049  vtxdginducedm1lem1  29063  vtxdginducedm1fi  29068  finsumvtxdg2ssteplem4  29072  pthdlem1  29290  crctcshlem3  29340  2wlkd  29457  2wlkond  29458  2trlond  29460  2pthd  29461  2pthond  29463  umgr2adedgwlkonALT  29468  0pth  29645  wlk2v2e  29677  3wlkd  29690  3trlond  29693  3pthd  29694  3pthond  29695  3spthond  29697  eupthvdres  29755  eulerpathpr  29760  konigsbergumgr  29771  konigsberglem5  29776  konigsberg  29777  ex-lcm  29978  isvciOLD  30100  isnvi  30133  blocni  30325  hmoval  30330  cncph  30339  ipasslem7  30356  siilem2  30372  normlem2  30631  normlem3  30632  normlem6  30635  h0elch  30775  hhssabloilem  30781  hhsssh  30789  spansnji  31166  nonbooli  31171  3oalem5  31186  3oalem6  31187  3oai  31188  mayetes3i  31249  nmcexi  31546  nmbdfnlb  31570  rnelshi  31579  cnlnadjlem5  31591  pjbdlni  31669  golem2  31792  goeqi  31793  dp2clq  32314  rpdp2cl  32315  rpdp2cl2  32316  dpmul100  32330  rpdpcl  32336  xrge0tsmsd  32479  pmtrto1cl  32528  psgnfzto1stlem  32529  fzto1st  32532  psgnfzto1st  32534  nn0omnd  32730  xrge0slmod  32733  qusima  32793  prmidl0  32843  fply1  32911  ply1degltdimlem  32995  ccfldextdgrr  33035  algextdeglem8  33069  circtopn  33115  circcn  33116  zarcmplem  33159  tpr2tp  33182  tpr2rico  33190  ordtprsval  33196  ordtprsuni  33197  ordtrestNEW  33199  ordtrest2NEWlem  33200  ordtrest2NEW  33201  ordtconnlem1  33202  mndpluscn  33204  xrge0pluscn  33218  xrge0mulc1cn  33219  xrge0haus  33222  lmlimxrge0  33226  lmxrge0  33230  qqhcn  33269  qqhucn  33270  esumex  33325  esumcst  33359  hasheuni  33381  esumcvg  33382  prsiga  33427  brsiga  33479  mbfmcnt  33565  sxbrsigalem3  33569  dya2iocuni  33580  dya2iocucvr  33581  sxbrsigalem1  33582  sxbrsiga  33587  eulerpartlemt  33668  fibp1  33698  coinflipprob  33776  coinfliprv  33779  ccatmulgnn0dir  33851  signswplusg  33864  hgt750lem2  33962  hgt750leme  33968  bnj105  34033  bnj918  34075  bnj95  34173  bnj852  34230  bnj865  34232  subfacp1lem1  34468  subfacp1lem3  34471  subfacp1lem5  34473  subfacp1lem6  34474  kur14lem7  34501  iisconn  34541  iillysconn  34542  cvmliftlem5  34578  cvmliftlem8  34581  cvmliftlem10  34583  cvmlift2lem9  34600  satfv0  34647  goalrlem  34685  goalr  34686  satffunlem2lem2  34695  circum  34957  iexpire  35009  altopex  35236  colinearex  35336  gg-cnfldex  35467  gg-cxpcn  35470  ssoninhaus  35636  cnndvlem2  35717  bj-prex  36224  bj-prfromadj  36229  bj-pinftyccb  36405  taupi  36507  isbasisrelowl  36542  relowlpssretop  36548  poimirlem29  36820  poimirlem30  36821  poimirlem31  36822  dvasin  36875  dvacos  36876  areacirc  36884  upixp  36900  fdc  36916  lmclim2  36929  cncfres  36936  heibor1lem  36980  rrnval  36998  rrnmet  37000  reheibor  37010  isdrngo2  37129  isrngohom  37136  idlval  37184  isidl  37185  igenval  37232  scottexf  37339  cnvepresex  37506  renegclALT  38136  ldualfvadd  38301  cmtfvalN  38383  cvrfval  38441  cdleme31fv  39564  cdlemk40  40091  cdlemk56  40145  dibopelvalN  40317  dibopelval2  40319  dibelval3  40321  diblsmopel  40345  cdlemn11a  40381  dihopelvalcpre  40422  dihpN  40510  hlhilsca  41109  hlhilip  41126  3factsumint1  41192  lcmineqlem23  41222  aks4d1p1p6  41244  aks4d1p1p5  41246  sn-0tie0  41614  itrere  41641  retire  41642  prjspval  41647  flt4lem5e  41700  acos1half  41717  mapfzcons2  41759  jm2.23  42037  jm2.27dlem2  42051  jm2.27dlem4  42053  rmydioph  42055  rmxdioph  42057  expdiophlem2  42063  expdioph  42064  aomclem6  42103  pwslnmlem0  42135  frlmpwfi  42142  mncn0  42183  aaitgo  42206  arearect  42266  areaquad  42267  omcl3g  42386  comptiunov2i  42759  frege110  43026  frege133  43049  scottex2  43306  radcnvrat  43375  uzmptshftfval  43407  dvradcnv2  43408  binomcxplemdvbinom  43414  binomcxplemcvg  43415  binomcxplemnotnn0  43417  rfcnpre1  44005  fcnre  44011  refsumcn  44016  refsum2cnlem1  44023  unirnmapsn  44211  infxrpnf  44454  iocopn  44531  icoopn  44536  mccl  44612  clim1fr1  44615  islptre  44633  sumnnodd  44644  lptre2pt  44654  limclner  44665  limclr  44669  expfac  44671  0cnf  44891  icccncfext  44901  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  itgsin0pilem1  44964  iblempty  44979  itgvol0  44982  stoweidlem47  45061  stoweidlem53  45067  stoweidlem57  45071  stoweidlem59  45073  wallispilem3  45081  wallispilem4  45082  wallispilem5  45083  wallispi  45084  stirlinglem1  45088  stirlinglem8  45095  stirlinglem12  45099  stirlinglem13  45100  stirlinglem14  45101  stirlinglem15  45102  dirkerper  45110  dirkercncflem2  45118  fourierdlem16  45137  fourierdlem21  45142  fourierdlem22  45143  fourierdlem36  45157  fourierdlem42  45163  fourierdlem71  45191  fourierdlem83  45203  fourierdlem102  45222  fourierdlem103  45223  fourierdlem104  45224  fourierdlem111  45231  fourierdlem112  45232  fourierdlem114  45234  sqwvfoura  45242  sqwvfourb  45243  fourierswlem  45244  fouriersw  45245  etransclem48  45296  salexct3  45356  salgencntex  45357  salgensscntex  45358  iooborel  45365  bor1sal  45369  gsumge0cl  45385  sge0tsms  45394  sge0isum  45441  nnfoctbdjlem  45469  isomenndlem  45544  mbfresmf  45753  incsmflem  45755  incsmf  45756  smfmbfcex  45774  decsmflem  45780  decsmf  45781  smflimlem1  45785  smfpimbor1lem2  45813  smf2id  45815  smfco  45816  smfpimcclem  45821  tworepnotupword  45898  sprsymrelfolem1  46458  sprbisymrel  46465  fmtno0prm  46524  fmtno1prm  46525  fmtno2prm  46526  fmtno3prm  46528  fmtno4prm  46541  m2prm  46557  m3prm  46558  m5prm  46564  m7prm  46566  lighneallem4a  46574  0evenALTV  46654  1oddALTV  46656  2evenALTV  46658  6even  46677  7odd  46678  8even  46679  9gbo  46740  strisomgrop  46806  ushrisomgr  46807  uspgrex  46826  lmod1zrnlvec  47262  zlmodzxzldeplem1  47268  zlmodzxzldeplem3  47270  zlmodzxzldeplem4  47271  zlmodzxzldep  47272  ldepsnlinclem1  47273  ldepsnlinclem2  47274  blennn0elnn  47350  nn0sumshdiglemA  47392  nn0sumshdiglemB  47393  itcovalpclem2  47444  itcovalt2lem2  47449  ackval42  47469  rrx2line  47513  rrx2linesl  47516  spheres  47519  2sphere  47522  2sphere0  47523  line2x  47527  line2y  47528  functhinclem1  47748  prsthinc  47761