Theorem eqeltri 2837

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

Syntax hints:   = wceq 1540   ∈ wcel 2108

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqeltrri  2838  3eltr4i  2854  intab  4978  axrep6g  5290  unisn2  5312  inex2  5318  vpwex  5377  ord3ex  5387  zfpair  5421  vsnex  5434  opex  5469  otex  5470  uniopel  5521  elvvuni  5762  isarep2  6658  fvex  6919  fvexi  6920  riotaex  7392  ovexi  7465  tpex  7766  oprabex  8001  oprabrexex2  8003  mpoexw  8103  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  tfrlem16  8433  1oex  8516  2oex  8517  1on  8518  1onOLD  8519  2on  8520  2onOLD  8521  3on  8524  4on  8525  oesuclem  8563  oecl  8575  o2p2e4  8579  nnecl  8651  1onnALT  8679  2onnALT  8681  3onn  8682  4onn  8683  mapsnf1o2  8934  sbthlem10  9132  cnvfi  9216  fnfi  9218  nnunifi  9327  imafiOLD  9354  pwfi  9357  xpfiOLD  9359  prfiALT  9364  tpfi  9365  fczfsuppd  9426  cantnfvalf  9705  oemapwe  9734  cantnffval2  9735  cnfcom3clem  9745  ssttrcl  9755  r1fin  9813  hta  9937  infxpenlem  10053  alephon  10109  alephfplem1  10144  dfac5lem4  10166  dfac5lem5  10167  dfac5lem4OLD  10168  kmlem10  10200  fin1a2lem10  10449  fin1a2lem12  10451  hsmexlem9  10465  axcc2lem  10476  domtriomlem  10482  axdc2lem  10488  axcclem  10497  brdom7disj  10571  brdom6disj  10572  iundom2g  10580  konigthlem  10608  canthwelem  10690  wunex2  10778  wunex3  10781  1nq  10968  1pr  11055  nrex1  11104  axcnex  11187  ax1cn  11189  pnfex  11314  mnfxr  11318  inelr  12256  cju  12262  nnexALT  12268  2nn  12339  2re  12340  2cn  12341  3nn  12345  3re  12346  3cn  12347  4nn  12349  4re  12350  4cn  12351  5nn  12352  5re  12353  5cn  12354  6nn  12355  6re  12356  6cn  12357  7nn  12358  7re  12359  7cn  12360  8nn  12361  8re  12362  8cn  12363  9nn  12364  9re  12365  9cn  12366  nn0ex  12532  zexALT  12633  nneo  12702  zeo  12704  deccl  12748  10re  12752  decnncl  12753  numnncl2  12756  decnncl2  12757  numsucc  12773  numma2c  12779  numadd  12780  numaddc  12781  nummul1c  12782  nummul2c  12783  decmul1  12797  qexALT  13006  xrex  13029  xnegex  13250  xnegcl  13255  ixxssxr  13399  fz0to4untppr  13670  fz0to5un2tp  13671  om2uzuzi  13990  ltweuz  14002  axdc4uzlem  14024  seqex  14044  seqexw  14058  m1expcl2  14126  faccl  14322  facwordi  14328  faclbnd2  14330  bccl  14361  hashen1  14409  hashrabrsn  14411  hashunlei  14464  hashpw  14475  tpf1o  14540  s1cli  14643  ccat2s1p1  14667  cats1un  14759  revs1  14803  cshwsexa  14862  cshwsexaOLD  14863  cats1cli  14896  cats1fvn  14897  crre  15153  remim  15156  climmpt  15607  sumex  15724  supcvg  15892  geo2lim  15911  prodex  15941  bpoly4  16095  ere  16125  eftlub  16145  efsep  16146  tan0  16187  ef01bndlem  16220  nn0o  16420  divalglem5  16434  divalglem9  16438  sadcf  16490  smupf  16515  crth  16815  phimullem  16816  pczpre  16885  pockthi  16945  prmreclem2  16955  igz  16972  0ramcl  17061  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  strle1  17195  ndxarg  17233  basendxnn  17257  plusgndxnn  17325  tsetndxnn  17398  plendxnn  17412  dsndxnn  17431  unifndxnn  17441  prdsbasex  17495  prdsds  17509  yonedalem3  18325  isposix  18370  isposixOLD  18371  plusffval  18659  issubmgm2  18716  efmnd1hash  18905  efmnd2hash  18907  smndex1bas  18919  smndex1sgrp  18921  smndex1mnd  18923  smndex1id  18924  smndex2dbas  18927  smndex2hbas  18929  grpsubfval  19001  mulgfval  19087  symg1hash  19407  symg2hash  19409  symgvalstruct  19414  symgvalstructOLD  19415  symgfisg  19486  psgnsn  19538  psgnprfval1  19540  odfval  19550  sylow2alem2  19636  efgsval2  19751  efgsp1  19755  pgpfaclem1  20101  dvdsrval  20361  isirred  20419  scaffval  20878  cnfldex  21367  xrsex  21395  pzriprnglem4  21495  pzriprnglem5  21496  pzriprnglem6  21497  pzriprng1ALT  21507  zlmlemOLD  21528  znle  21551  znidomb  21580  cnmsgnsubg  21595  refld  21637  ipffval  21666  psrbag0  22086  psrbagsn  22087  psr1baslem  22186  mat1dimbas  22478  mat1dimscm  22481  mat1f1o  22484  mat1rhmelval  22486  m2detleib  22637  pmatcoe1fsupp  22707  indistopon  23008  iccordt  23222  conncompid  23439  ptbasfi  23589  ptcmpfi  23821  ustfn  24210  ust0  24228  ustn0  24229  tmslem  24494  tmslemOLD  24495  nmfval  24601  tnglemOLD  24654  cnbl0  24794  cnopn  24807  remet  24811  re2ndc  24822  zcld  24835  icccmp  24847  xrge0gsumle  24855  xrge0tsms  24856  xmetdcn  24860  divcnOLD  24890  divcn  24892  expcn  24896  expcnOLD  24898  iiconn  24913  idcncf  24944  cnmpopc  24955  cnrehmeo  24984  cnrehmeoOLD  24985  cnheiborlem  24986  rellycmp  24989  bndth  24990  evth2  24992  cnrlmod  25176  cnrlvec  25177  cncmet  25356  ishl2  25404  ehleudis  25452  ehleudisval  25453  finiunmbl  25579  ioombl1lem4  25596  vitalilem4  25646  vitalilem5  25647  ismbf2d  25675  mbfimaopnlem  25690  mbfi1fseqlem6  25755  itgex  25805  bddmulibl  25874  ditgex  25887  recnperf  25940  dvcnvrelem2  26057  ftc1  26083  mdegcl  26108  plyeq0lem  26249  aaliou3lem4  26388  dvradcnv  26464  sincn  26488  coscn  26489  tanabsge  26548  circsubm  26595  reloggim  26641  logcn  26689  dvloglem  26690  logdmopn  26691  dvlog2  26695  2irrexpq  26773  cxpcn  26787  cxpcnOLD  26788  cxpcn3  26791  resqrtcn  26792  2logb9irrALT  26841  2irrexpqALT  26843  atanrecl  26954  atan1  26971  atansopn  26975  birthdaylem1  26994  birthday  26997  emcllem4  27042  emcllem6  27044  lgamgulmlem6  27077  basellem6  27129  ppiublem1  27246  bposlem6  27333  bposlem8  27335  lgslem4  27344  lgsdir2lem2  27370  selberglem1  27589  selberglem3  27591  selberg  27592  selbergs  27618  qdrng  27664  0sno  27871  1sno  27872  lrrecse  27975  precsexlem11  28241  seqsex  28291  nnsex  28323  n0sbday  28354  n0subs  28360  n0p1nns  28361  dfnns2  28362  zsex  28366  zs12ex  28422  edgfndxnn  29007  structvtxvallem  29037  usgrexmpllem  29277  usgrexmpl  29280  uhgrspan1  29320  upgrres  29323  umgrres  29324  usgrres  29325  upgrres1  29330  umgrres1  29331  usgrres1  29332  fusgrfis  29347  cusgrres  29466  vtxdlfgrval  29503  vtxdusgr0edgnelALT  29514  umgr2v2e  29543  vtxdginducedm1lem1  29557  vtxdginducedm1fi  29562  finsumvtxdg2ssteplem4  29566  pthdlem1  29786  crctcshlem3  29839  2wlkd  29956  2wlkond  29957  2trlond  29959  2pthd  29960  2pthond  29962  umgr2adedgwlkonALT  29967  0pth  30144  wlk2v2e  30176  3wlkd  30189  3trlond  30192  3pthd  30193  3pthond  30194  3spthond  30196  eupthvdres  30254  eulerpathpr  30259  konigsbergumgr  30270  konigsberglem5  30275  konigsberg  30276  ex-lcm  30477  isvciOLD  30599  isnvi  30632  blocni  30824  hmoval  30829  cncph  30838  ipasslem7  30855  siilem2  30871  normlem2  31130  normlem3  31131  normlem6  31134  h0elch  31274  hhssabloilem  31280  hhsssh  31288  spansnji  31665  nonbooli  31670  3oalem5  31685  3oalem6  31686  3oai  31687  mayetes3i  31748  nmcexi  32045  nmbdfnlb  32069  rnelshi  32078  cnlnadjlem5  32090  pjbdlni  32168  golem2  32291  goeqi  32292  dp2clq  32863  rpdp2cl  32864  rpdp2cl2  32865  dpmul100  32879  rpdpcl  32885  chnub  33002  xrge0tsmsd  33065  pmtrto1cl  33119  psgnfzto1stlem  33120  fzto1st  33123  psgnfzto1st  33125  nn0omnd  33373  xrge0slmod  33376  qusima  33436  prmidl0  33478  fply1  33584  ply1degltdimlem  33673  ccfldextdgrr  33722  algextdeglem8  33765  constrfin  33787  2sqr3minply  33791  circtopn  33836  circcn  33837  zarcmplem  33880  tpr2tp  33903  tpr2rico  33911  ordtprsval  33917  ordtprsuni  33918  ordtrestNEW  33920  ordtrest2NEWlem  33921  ordtrest2NEW  33922  ordtconnlem1  33923  mndpluscn  33925  xrge0pluscn  33939  xrge0mulc1cn  33940  xrge0haus  33943  lmlimxrge0  33947  lmxrge0  33951  qqhcn  33992  qqhucn  33993  esumex  34030  esumcst  34064  hasheuni  34086  esumcvg  34087  prsiga  34132  brsiga  34184  mbfmcnt  34270  sxbrsigalem3  34274  dya2iocuni  34285  dya2iocucvr  34286  sxbrsigalem1  34287  sxbrsiga  34292  eulerpartlemt  34373  fibp1  34403  coinflipprob  34482  coinfliprv  34485  ccatmulgnn0dir  34557  signswplusg  34570  hgt750lem2  34667  hgt750leme  34673  bnj105  34738  bnj918  34780  bnj95  34878  bnj852  34935  bnj865  34937  subfacp1lem1  35184  subfacp1lem3  35187  subfacp1lem5  35189  subfacp1lem6  35190  kur14lem7  35217  iisconn  35257  iillysconn  35258  cvmliftlem5  35294  cvmliftlem8  35297  cvmliftlem10  35299  cvmlift2lem9  35316  satfv0  35363  goalrlem  35401  goalr  35402  satffunlem2lem2  35411  circum  35679  iexpire  35735  altopex  35961  colinearex  36061  ssoninhaus  36449  cnndvlem2  36539  bj-prex  37041  bj-prfromadj  37046  bj-pinftyccb  37222  taupi  37324  isbasisrelowl  37359  relowlpssretop  37365  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  dvasin  37711  dvacos  37712  areacirc  37720  upixp  37736  fdc  37752  lmclim2  37765  cncfres  37772  heibor1lem  37816  rrnval  37834  rrnmet  37836  reheibor  37846  isdrngo2  37965  isrngohom  37972  idlval  38020  isidl  38021  igenval  38068  scottexf  38175  cnvepresex  38335  renegclALT  38964  ldualfvadd  39129  cmtfvalN  39211  cvrfval  39269  cdleme31fv  40392  cdlemk40  40919  cdlemk56  40973  dibopelvalN  41145  dibopelval2  41147  dibelval3  41149  diblsmopel  41173  cdlemn11a  41209  dihopelvalcpre  41250  dihpN  41338  hlhilsca  41937  hlhilip  41954  3factsumint1  42022  lcmineqlem23  42052  aks4d1p1p6  42074  aks4d1p1p5  42076  aks6d1c6isolem2  42176  itrere  42353  acos1half  42388  redvmptabs  42390  readvrec2  42391  sn-0tie0  42469  sn-itrere  42498  sn-retire  42499  prjspval  42613  flt4lem5e  42666  sn-isghm  42683  mapfzcons2  42730  jm2.23  43008  jm2.27dlem2  43022  jm2.27dlem4  43024  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  aomclem6  43071  pwslnmlem0  43103  frlmpwfi  43110  mncn0  43151  aaitgo  43174  arearect  43227  areaquad  43228  omcl3g  43347  comptiunov2i  43719  frege110  43986  frege133  44009  scottex2  44264  radcnvrat  44333  uzmptshftfval  44365  dvradcnv2  44366  binomcxplemdvbinom  44372  binomcxplemcvg  44373  binomcxplemnotnn0  44375  rfcnpre1  45024  fcnre  45030  refsumcn  45035  refsum2cnlem1  45042  unirnmapsn  45219  infxrpnf  45457  iocopn  45533  icoopn  45538  mccl  45613  clim1fr1  45616  islptre  45634  sumnnodd  45645  lptre2pt  45655  limclner  45666  limclr  45670  expfac  45672  0cnf  45892  icccncfext  45902  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  itgsin0pilem1  45965  iblempty  45980  itgvol0  45983  stoweidlem47  46062  stoweidlem53  46068  stoweidlem57  46072  stoweidlem59  46074  wallispilem3  46082  wallispilem4  46083  wallispilem5  46084  wallispi  46085  stirlinglem1  46089  stirlinglem8  46096  stirlinglem12  46100  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  dirkerper  46111  dirkercncflem2  46119  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem36  46158  fourierdlem42  46164  fourierdlem71  46192  fourierdlem83  46204  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem114  46235  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  etransclem48  46297  salexct3  46357  salgencntex  46358  salgensscntex  46359  iooborel  46366  bor1sal  46370  gsumge0cl  46386  sge0tsms  46395  sge0isum  46442  nnfoctbdjlem  46470  isomenndlem  46545  mbfresmf  46754  incsmflem  46756  incsmf  46757  smfmbfcex  46775  decsmflem  46781  decsmf  46782  smflimlem1  46786  smfpimbor1lem2  46814  smf2id  46816  smfco  46817  smfpimcclem  46822  tworepnotupword  46901  sprsymrelfolem1  47479  sprbisymrel  47486  fmtno0prm  47545  fmtno1prm  47546  fmtno2prm  47547  fmtno3prm  47549  fmtno4prm  47562  m2prm  47578  m3prm  47579  m5prm  47585  m7prm  47587  lighneallem4a  47595  0evenALTV  47675  1oddALTV  47677  2evenALTV  47679  6even  47698  7odd  47699  8even  47700  9gbo  47761  opstrgric  47895  ushggricedg  47896  grtri  47907  usgrexmpl1  47981  usgrexmpl1vtx  47982  usgrexmpl1edg  47983  usgrexmpl2  47986  usgrexmpl2vtx  47987  usgrexmpl2edg  47988  uspgrex  48066  lmod1zrnlvec  48411  zlmodzxzldeplem1  48417  zlmodzxzldeplem3  48419  zlmodzxzldeplem4  48420  zlmodzxzldep  48421  ldepsnlinclem1  48422  ldepsnlinclem2  48423  blennn0elnn  48498  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  itcovalpclem2  48592  itcovalt2lem2  48597  ackval42  48617  rrx2line  48661  rrx2linesl  48664  spheres  48667  2sphere  48670  2sphere0  48671  line2x  48675  line2y  48676  functhinclem1  49093  prsthinc  49111  setc1oterm  49134  functermc2  49141