Theorem eqeltri 2879

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

Syntax hints:   = wceq 1522   ∈ wcel 2081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-clel 2863

This theorem is referenced by:  eqeltrri  2880  3eltr4i  2896  intab  4812  unisn2  5107  inex2  5113  vpwex  5169  ord3ex  5178  zfpair  5213  opex  5248  otex  5249  uniopel  5297  elvvuni  5514  predasetex  6038  isarep2  6313  fvex  6551  fvexi  6552  riotaex  6981  ovexi  7049  tpex  7327  oprabex  7533  oprabrexex2  7535  mpoexw  7632  tfrlem16  7881  1on  7960  2on  7962  2oex  7963  3on  7965  4on  7966  oesuclem  8001  oecl  8013  nnecl  8089  1onn  8115  2onn  8116  3onn  8117  4onn  8118  mapsnf1o2  8307  sbthlem10  8483  nnunifi  8615  xpfi  8635  prfi  8639  tpfi  8640  fnfi  8642  pwfi  8665  fczfsuppd  8697  inf0  8930  cantnfvalf  8974  oemapwe  9003  cantnffval2  9004  cnfcom3clem  9014  r1fin  9048  hta  9172  infxpenlem  9285  alephon  9341  alephfplem1  9376  dfac5lem4  9398  dfac5lem5  9399  kmlem10  9431  fin1a2lem10  9677  fin1a2lem12  9679  hsmexlem9  9693  axcc2lem  9704  domtriomlem  9710  axdc2lem  9716  axcclem  9725  brdom7disj  9799  brdom6disj  9800  iundom2g  9808  konigthlem  9836  canthwelem  9918  wunex2  10006  wunex3  10009  1nq  10196  1pr  10283  nrex1  10332  axcnex  10415  ax1cn  10417  pnfex  10540  mnfxr  10545  inelr  11476  cju  11482  nnexALT  11488  2nn  11558  2re  11559  2cn  11560  3nn  11564  3re  11565  3cn  11566  4nn  11568  4re  11569  4cn  11570  5nn  11571  5re  11572  5cn  11573  6nn  11574  6re  11575  6cn  11576  7nn  11577  7re  11578  7cn  11579  8nn  11580  8re  11581  8cn  11582  9nn  11583  9re  11584  9cn  11585  nn0ex  11751  zexALT  11849  nneo  11915  zeo  11917  deccl  11962  10re  11966  decnncl  11967  numnncl2  11970  decnncl2  11971  numsucc  11987  numma2c  11993  numadd  11994  numaddc  11995  nummul1c  11996  nummul2c  11997  decmul1  12011  qexALT  12213  xrex  12236  xnegex  12451  xnegcl  12456  ixxssxr  12600  om2uzuzi  13167  ltweuz  13179  axdc4uzlem  13201  seqex  13221  seqexw  13235  m1expcl2  13301  faccl  13493  facwordi  13499  faclbnd2  13501  bccl  13532  hashen1  13580  hashrabrsn  13581  hashunlei  13634  hashpw  13645  s1cli  13803  cats1un  13919  revs1  13963  cshwsexa  14022  cats1cli  14055  cats1fvn  14056  crre  14307  remim  14310  climmpt  14762  sumex  14878  supcvg  15044  geo2lim  15064  prodex  15094  bpoly4  15246  ere  15275  eftlub  15295  efsep  15296  tan0  15337  ef01bndlem  15370  nn0o  15567  divalglem5  15581  divalglem9  15585  sadcf  15635  smupf  15660  crth  15944  phimullem  15945  pczpre  16013  pockthi  16072  prmreclem2  16082  igz  16099  0ramcl  16188  1259lem1  16293  1259lem2  16294  1259lem3  16295  1259lem4  16296  1259lem5  16297  1259prm  16298  2503lem1  16299  2503lem2  16300  2503lem3  16301  2503prm  16302  4001lem1  16303  4001lem2  16304  4001lem3  16305  4001lem4  16306  4001prm  16307  ndxarg  16337  basendxnn  16377  strle1  16421  prdsbasex  16553  prdsds  16566  yonedalem3  17359  isposix  17396  plusffval  17686  grpsubfval  17904  mulgfval  17983  symg1hash  18254  symg2hash  18256  symgfisg  18327  psgnsn  18379  psgnprfval1  18381  odfval  18391  sylow2alem2  18473  efgsval2  18586  efgsp1  18590  dvdsrval  19085  isirred  19139  scaffval  19342  psrbag0  19961  psrbagsn  19962  psr1baslem  20036  xrsex  20242  zlmlem  20346  znle  20365  znidomb  20390  cnmsgnsubg  20403  refld  20445  ipffval  20474  mat1dimbas  20765  mat1dimscm  20768  mat1f1o  20771  mat1rhmelval  20773  m2detleib  20924  pmatcoe1fsupp  20993  indistopon  21293  iccordt  21506  conncompid  21723  ptbasfi  21873  ptcmpfi  22105  ustfn  22493  ust0  22511  ustn0  22512  tmslem  22775  nmfval  22881  tnglem  22932  cnbl0  23065  cnopn  23078  remet  23081  re2ndc  23092  zcld  23104  icccmp  23116  xrge0gsumle  23124  xrge0tsms  23125  xmetdcn  23129  divcn  23159  expcn  23163  iiconn  23178  cnmpopc  23215  cnrehmeo  23240  cnheiborlem  23241  rellycmp  23244  bndth  23245  evth2  23247  cnrlmod  23430  cnrlvec  23431  cncmet  23608  ishl2  23656  ehleudis  23704  ehleudisval  23705  finiunmbl  23828  ioombl1lem4  23845  vitalilem4  23895  vitalilem5  23896  ismbf2d  23924  mbfimaopnlem  23939  mbfi1fseqlem6  24004  itgex  24054  bddmulibl  24122  ditgex  24133  recnperf  24186  dvcnvrelem2  24298  ftc1  24322  mdegcl  24346  plyeq0lem  24483  aaliou3lem4  24618  dvradcnv  24692  sincn  24715  coscn  24716  tanabsge  24775  circsubm  24818  reloggim  24863  logcn  24911  dvloglem  24912  logdmopn  24913  dvlog2  24917  2irrexpq  24994  cxpcn  25007  cxpcn3  25010  resqrtcn  25011  2logb9irrALT  25057  2irrexpqALT  25059  atanrecl  25170  atan1  25187  atansopn  25191  birthdaylem1  25211  birthday  25214  emcllem4  25258  emcllem6  25260  lgamgulmlem6  25293  basellem6  25345  ppiublem1  25460  bposlem6  25547  bposlem8  25549  lgslem4  25558  lgsdir2lem2  25584  selberglem1  25803  selberglem3  25805  selberg  25806  selbergs  25832  qdrng  25878  edgfndxnn  26460  structvtxvallem  26488  usgrexmpllem  26725  usgrexmpl  26728  uhgrspan1  26768  upgrres  26771  umgrres  26772  usgrres  26773  upgrres1  26778  umgrres1  26779  usgrres1  26780  cusgrres  26913  vtxdlfgrval  26950  vtxdusgr0edgnelALT  26961  umgr2v2e  26990  vtxdginducedm1lem1  27004  vtxdginducedm1fi  27009  finsumvtxdg2ssteplem4  27013  pthdlem1  27234  crctcshlem3  27284  2wlkd  27402  2wlkond  27403  2trlond  27405  2pthd  27406  2pthond  27408  umgr2adedgwlkonALT  27413  0pth  27591  wlk2v2e  27623  3wlkd  27636  3trlond  27639  3pthd  27640  3pthond  27641  3spthond  27643  eupthvdres  27702  eulerpathpr  27707  konigsbergumgr  27720  konigsberglem5  27725  konigsberg  27726  ex-lcm  27929  isvciOLD  28048  isnvi  28081  blocni  28273  hmoval  28278  cncph  28287  ipasslem7  28304  siilem2  28320  normlem2  28579  normlem3  28580  normlem6  28583  h0elch  28723  hhssabloilem  28729  hhsssh  28737  spansnji  29114  nonbooli  29119  3oalem5  29134  3oalem6  29135  3oai  29136  mayetes3i  29197  nmcexi  29494  nmbdfnlb  29518  rnelshi  29527  cnlnadjlem5  29539  pjbdlni  29617  golem2  29740  goeqi  29741  dp2clq  30241  rpdp2cl  30242  rpdp2cl2  30243  dpmul100  30257  rpdpcl  30263  xrge0tsmsd  30503  nn0omnd  30568  xrge0slmod  30571  fply1  30579  ccfldextdgrr  30661  pmtrto1cl  30663  psgnfzto1stlem  30664  fzto1st  30667  psgnfzto1st  30669  circtopn  30718  circcn  30719  tpr2tp  30764  tpr2rico  30772  ordtprsval  30778  ordtprsuni  30779  ordtrestNEW  30781  ordtrest2NEWlem  30782  ordtrest2NEW  30783  ordtconnlem1  30784  mndpluscn  30786  xrge0pluscn  30800  xrge0mulc1cn  30801  xrge0haus  30804  lmlimxrge0  30808  lmxrge0  30812  qqhcn  30849  qqhucn  30850  esumex  30905  esumcst  30939  hasheuni  30961  esumcvg  30962  prsiga  31007  brsiga  31059  mbfmcnt  31143  sxbrsigalem3  31147  dya2iocuni  31158  dya2iocucvr  31159  sxbrsigalem1  31160  sxbrsiga  31165  eulerpartlemt  31246  fibp1  31276  coinflipprob  31354  coinfliprv  31357  ccatmulgnn0dir  31429  signswplusg  31442  hgt750lem2  31540  hgt750leme  31546  bnj105  31611  bnj918  31654  bnj95  31752  bnj852  31809  bnj865  31811  subfacp1lem1  32034  subfacp1lem3  32037  subfacp1lem5  32039  subfacp1lem6  32040  kur14lem7  32067  iisconn  32107  iillysconn  32108  cvmliftlem5  32144  cvmliftlem8  32147  cvmliftlem10  32149  cvmlift2lem9  32166  satfv0  32213  goalrlem  32251  goalr  32252  satffunlem2lem2  32261  circum  32525  iexpire  32575  trpredex  32685  altopex  33030  colinearex  33130  ssoninhaus  33405  cnndvlem2  33486  bj-pinftyccb  34061  taupi  34135  isbasisrelowl  34170  relowlpssretop  34176  poimirlem29  34452  poimirlem30  34453  poimirlem31  34454  dvasin  34509  dvacos  34510  areacirc  34518  upixp  34536  fdc  34552  lmclim2  34565  idcncf  34570  cncfres  34575  heibor1lem  34619  rrnval  34637  rrnmet  34639  reheibor  34649  isdrngo2  34768  isrngohom  34775  idlval  34823  isidl  34824  igenval  34871  scottexf  34978  cnvepresex  35123  renegclALT  35630  ldualfvadd  35795  cmtfvalN  35877  cvrfval  35935  cdleme31fv  37057  cdlemk40  37584  cdlemk56  37638  dibopelvalN  37810  dibopelval2  37812  dibelval3  37814  diblsmopel  37838  cdlemn11a  37874  dihopelvalcpre  37915  dihpN  38003  hlhilsca  38602  hlhilip  38615  prjspval  38750  0prjspn  38767  mapfzcons2  38801  jm2.23  39078  jm2.27dlem2  39092  jm2.27dlem4  39094  rmydioph  39096  rmxdioph  39098  expdiophlem2  39104  expdioph  39105  aomclem6  39144  pwslnmlem0  39176  frlmpwfi  39183  mncn0  39224  aaitgo  39247  arearect  39307  areaquad  39308  comptiunov2i  39536  frege110  39804  frege133  39827  scottex2  40078  radcnvrat  40184  uzmptshftfval  40216  dvradcnv2  40217  binomcxplemdvbinom  40223  binomcxplemcvg  40224  binomcxplemnotnn0  40226  rfcnpre1  40815  fcnre  40821  refsumcn  40826  refsum2cnlem1  40833  unirnmapsn  41017  infxrpnf  41263  iocopn  41338  icoopn  41343  mccl  41421  clim1fr1  41424  islptre  41442  sumnnodd  41453  lptre2pt  41463  limclner  41474  limclr  41478  expfac  41480  0cnf  41701  icccncfext  41711  ioodvbdlimc1lem2  41758  ioodvbdlimc2lem  41760  itgsin0pilem1  41776  iblempty  41791  itgvol0  41794  stoweidlem47  41874  stoweidlem53  41880  stoweidlem57  41884  stoweidlem59  41886  wallispilem3  41894  wallispilem4  41895  wallispilem5  41896  wallispi  41897  stirlinglem1  41901  stirlinglem8  41908  stirlinglem12  41912  stirlinglem13  41913  stirlinglem14  41914  stirlinglem15  41915  dirkerper  41923  dirkercncflem2  41931  fourierdlem16  41950  fourierdlem21  41955  fourierdlem22  41956  fourierdlem36  41970  fourierdlem42  41976  fourierdlem71  42004  fourierdlem83  42016  fourierdlem102  42035  fourierdlem103  42036  fourierdlem104  42037  fourierdlem111  42044  fourierdlem112  42045  fourierdlem114  42047  sqwvfoura  42055  sqwvfourb  42056  fourierswlem  42057  fouriersw  42058  etransclem48  42109  salexct3  42167  salgencntex  42168  salgensscntex  42169  iooborel  42176  bor1sal  42180  gsumge0cl  42195  sge0tsms  42204  sge0isum  42251  nnfoctbdjlem  42279  isomenndlem  42354  mbfresmf  42558  incsmflem  42560  incsmf  42561  smfmbfcex  42578  decsmflem  42584  decsmf  42585  smflimlem1  42589  smfpimbor1lem2  42616  smf2id  42618  smfco  42619  smfpimcclem  42623  sprsymrelfolem1  43136  sprbisymrel  43143  fmtno0prm  43202  fmtno1prm  43203  fmtno2prm  43204  fmtno3prm  43206  fmtno4prm  43219  m2prm  43235  m3prm  43236  m5prm  43243  m7prm  43246  lighneallem4a  43255  0evenALTV  43335  1oddALTV  43337  2evenALTV  43339  6even  43358  7odd  43359  8even  43360  9gbo  43421  strisomgrop  43487  ushrisomgr  43488  uspgrex  43507  issubmgm2  43539  lmod1zrnlvec  44029  zlmodzxzldeplem1  44035  zlmodzxzldeplem3  44037  zlmodzxzldeplem4  44038  zlmodzxzldep  44039  ldepsnlinclem1  44040  ldepsnlinclem2  44041  blennn0elnn  44118  nn0sumshdiglemA  44160  nn0sumshdiglemB  44161  rrx2line  44208  rrx2linesl  44211  spheres  44214  2sphere  44217  2sphere0  44218  line2x  44222  line2y  44223