Theorem eqeltri 2911

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

Syntax hints:   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895

This theorem is referenced by:  eqeltrri  2912  3eltr4i  2928  intab  4908  unisn2  5218  inex2  5224  vpwex  5280  ord3ex  5290  zfpair  5324  opex  5358  otex  5359  uniopel  5408  elvvuni  5630  predasetex  6165  isarep2  6445  fvex  6685  fvexi  6686  riotaex  7120  ovexi  7192  tpex  7472  oprabex  7679  oprabrexex2  7681  mpoexw  7778  tfrlem16  8031  1on  8111  2on  8113  2oex  8114  3on  8116  4on  8117  oesuclem  8152  oecl  8164  o2p2e4  8168  nnecl  8241  1onn  8267  2onn  8268  3onn  8269  4onn  8270  mapsnf1o2  8460  sbthlem10  8638  nnunifi  8771  xpfi  8791  prfi  8795  tpfi  8796  fnfi  8798  pwfi  8821  fczfsuppd  8853  inf0  9086  cantnfvalf  9130  oemapwe  9159  cantnffval2  9160  cnfcom3clem  9170  r1fin  9204  hta  9328  infxpenlem  9441  alephon  9497  alephfplem1  9532  dfac5lem4  9554  dfac5lem5  9555  kmlem10  9587  fin1a2lem10  9833  fin1a2lem12  9835  hsmexlem9  9849  axcc2lem  9860  domtriomlem  9866  axdc2lem  9872  axcclem  9881  brdom7disj  9955  brdom6disj  9956  iundom2g  9964  konigthlem  9992  canthwelem  10074  wunex2  10162  wunex3  10165  1nq  10352  1pr  10439  nrex1  10488  axcnex  10571  ax1cn  10573  pnfex  10696  mnfxr  10700  inelr  11630  cju  11636  nnexALT  11642  2nn  11713  2re  11714  2cn  11715  3nn  11719  3re  11720  3cn  11721  4nn  11723  4re  11724  4cn  11725  5nn  11726  5re  11727  5cn  11728  6nn  11729  6re  11730  6cn  11731  7nn  11732  7re  11733  7cn  11734  8nn  11735  8re  11736  8cn  11737  9nn  11738  9re  11739  9cn  11740  nn0ex  11906  zexALT  12004  nneo  12069  zeo  12071  deccl  12116  10re  12120  decnncl  12121  numnncl2  12124  decnncl2  12125  numsucc  12141  numma2c  12147  numadd  12148  numaddc  12149  nummul1c  12150  nummul2c  12151  decmul1  12165  qexALT  12366  xrex  12389  xnegex  12604  xnegcl  12609  ixxssxr  12753  om2uzuzi  13320  ltweuz  13332  axdc4uzlem  13354  seqex  13374  seqexw  13388  m1expcl2  13454  faccl  13646  facwordi  13652  faclbnd2  13654  bccl  13685  hashen1  13734  hashrabrsn  13736  hashunlei  13789  hashpw  13800  s1cli  13961  ccat2s1p1  13987  cats1un  14085  revs1  14129  cshwsexa  14188  cats1cli  14221  cats1fvn  14222  crre  14475  remim  14478  climmpt  14930  sumex  15046  supcvg  15213  geo2lim  15233  prodex  15263  bpoly4  15415  ere  15444  eftlub  15464  efsep  15465  tan0  15506  ef01bndlem  15539  nn0o  15736  divalglem5  15750  divalglem9  15754  sadcf  15804  smupf  15829  crth  16117  phimullem  16118  pczpre  16186  pockthi  16245  prmreclem2  16255  igz  16272  0ramcl  16361  1259lem1  16466  1259lem2  16467  1259lem3  16468  1259lem4  16469  1259lem5  16470  1259prm  16471  2503lem1  16472  2503lem2  16473  2503lem3  16474  2503prm  16475  4001lem1  16476  4001lem2  16477  4001lem3  16478  4001lem4  16479  4001prm  16480  ndxarg  16510  basendxnn  16550  strle1  16594  prdsbasex  16726  prdsds  16739  yonedalem3  17532  isposix  17569  plusffval  17860  efmnd1hash  18059  efmnd2hash  18061  smndex1bas  18073  smndex1sgrp  18075  smndex1mnd  18077  smndex1id  18078  smndex2dbas  18081  smndex2hbas  18083  grpsubfval  18149  mulgfval  18228  symg1hash  18520  symg2hash  18522  symgvalstruct  18527  symgfisg  18598  psgnsn  18650  psgnprfval1  18652  odfval  18662  sylow2alem2  18745  efgsval2  18861  efgsp1  18865  pgpfaclem1  19205  dvdsrval  19397  isirred  19451  scaffval  19654  psrbag0  20276  psrbagsn  20277  psr1baslem  20355  xrsex  20562  zlmlem  20666  znle  20685  znidomb  20710  cnmsgnsubg  20723  refld  20765  ipffval  20794  mat1dimbas  21083  mat1dimscm  21086  mat1f1o  21089  mat1rhmelval  21091  m2detleib  21242  pmatcoe1fsupp  21311  indistopon  21611  iccordt  21824  conncompid  22041  ptbasfi  22191  ptcmpfi  22423  ustfn  22812  ust0  22830  ustn0  22831  tmslem  23094  nmfval  23200  tnglem  23251  cnbl0  23384  cnopn  23397  remet  23400  re2ndc  23411  zcld  23423  icccmp  23435  xrge0gsumle  23443  xrge0tsms  23444  xmetdcn  23448  divcn  23478  expcn  23482  iiconn  23497  cnmpopc  23534  cnrehmeo  23559  cnheiborlem  23560  rellycmp  23563  bndth  23564  evth2  23566  cnrlmod  23749  cnrlvec  23750  cncmet  23927  ishl2  23975  ehleudis  24023  ehleudisval  24024  finiunmbl  24147  ioombl1lem4  24164  vitalilem4  24214  vitalilem5  24215  ismbf2d  24243  mbfimaopnlem  24258  mbfi1fseqlem6  24323  itgex  24373  bddmulibl  24441  ditgex  24452  recnperf  24505  dvcnvrelem2  24617  ftc1  24641  mdegcl  24665  plyeq0lem  24802  aaliou3lem4  24937  dvradcnv  25011  sincn  25034  coscn  25035  tanabsge  25094  circsubm  25139  reloggim  25184  logcn  25232  dvloglem  25233  logdmopn  25234  dvlog2  25238  2irrexpq  25315  cxpcn  25328  cxpcn3  25331  resqrtcn  25332  2logb9irrALT  25378  2irrexpqALT  25380  atanrecl  25491  atan1  25508  atansopn  25512  birthdaylem1  25531  birthday  25534  emcllem4  25578  emcllem6  25580  lgamgulmlem6  25613  basellem6  25665  ppiublem1  25780  bposlem6  25867  bposlem8  25869  lgslem4  25878  lgsdir2lem2  25904  selberglem1  26123  selberglem3  26125  selberg  26126  selbergs  26152  qdrng  26198  edgfndxnn  26779  structvtxvallem  26807  usgrexmpllem  27044  usgrexmpl  27047  uhgrspan1  27087  upgrres  27090  umgrres  27091  usgrres  27092  upgrres1  27097  umgrres1  27098  usgrres1  27099  fusgrfis  27114  cusgrres  27232  vtxdlfgrval  27269  vtxdusgr0edgnelALT  27280  umgr2v2e  27309  vtxdginducedm1lem1  27323  vtxdginducedm1fi  27328  finsumvtxdg2ssteplem4  27332  pthdlem1  27549  crctcshlem3  27599  2wlkd  27717  2wlkond  27718  2trlond  27720  2pthd  27721  2pthond  27723  umgr2adedgwlkonALT  27728  0pth  27906  wlk2v2e  27938  3wlkd  27951  3trlond  27954  3pthd  27955  3pthond  27956  3spthond  27958  eupthvdres  28016  eulerpathpr  28021  konigsbergumgr  28032  konigsberglem5  28037  konigsberg  28038  ex-lcm  28239  isvciOLD  28359  isnvi  28392  blocni  28584  hmoval  28589  cncph  28598  ipasslem7  28615  siilem2  28631  normlem2  28890  normlem3  28891  normlem6  28894  h0elch  29034  hhssabloilem  29040  hhsssh  29048  spansnji  29425  nonbooli  29430  3oalem5  29445  3oalem6  29446  3oai  29447  mayetes3i  29508  nmcexi  29805  nmbdfnlb  29829  rnelshi  29838  cnlnadjlem5  29850  pjbdlni  29928  golem2  30051  goeqi  30052  dp2clq  30559  rpdp2cl  30560  rpdp2cl2  30561  dpmul100  30575  rpdpcl  30581  xrge0tsmsd  30694  pmtrto1cl  30743  psgnfzto1stlem  30744  fzto1st  30747  psgnfzto1st  30749  nn0omnd  30916  xrge0slmod  30919  fply1  30933  ccfldextdgrr  31059  circtopn  31103  circcn  31104  tpr2tp  31149  tpr2rico  31157  ordtprsval  31163  ordtprsuni  31164  ordtrestNEW  31166  ordtrest2NEWlem  31167  ordtrest2NEW  31168  ordtconnlem1  31169  mndpluscn  31171  xrge0pluscn  31185  xrge0mulc1cn  31186  xrge0haus  31189  lmlimxrge0  31193  lmxrge0  31197  qqhcn  31234  qqhucn  31235  esumex  31290  esumcst  31324  hasheuni  31346  esumcvg  31347  prsiga  31392  brsiga  31444  mbfmcnt  31528  sxbrsigalem3  31532  dya2iocuni  31543  dya2iocucvr  31544  sxbrsigalem1  31545  sxbrsiga  31550  eulerpartlemt  31631  fibp1  31661  coinflipprob  31739  coinfliprv  31742  ccatmulgnn0dir  31814  signswplusg  31827  hgt750lem2  31925  hgt750leme  31931  bnj105  31996  bnj918  32039  bnj95  32138  bnj852  32195  bnj865  32197  subfacp1lem1  32428  subfacp1lem3  32431  subfacp1lem5  32433  subfacp1lem6  32434  kur14lem7  32461  iisconn  32501  iillysconn  32502  cvmliftlem5  32538  cvmliftlem8  32541  cvmliftlem10  32543  cvmlift2lem9  32560  satfv0  32607  goalrlem  32645  goalr  32646  satffunlem2lem2  32655  circum  32919  iexpire  32969  trpredex  33078  altopex  33423  colinearex  33523  ssoninhaus  33798  cnndvlem2  33879  bj-pinftyccb  34505  taupi  34606  isbasisrelowl  34641  relowlpssretop  34647  poimirlem29  34923  poimirlem30  34924  poimirlem31  34925  dvasin  34980  dvacos  34981  areacirc  34989  upixp  35006  fdc  35022  lmclim2  35035  idcncf  35040  cncfres  35045  heibor1lem  35089  rrnval  35107  rrnmet  35109  reheibor  35119  isdrngo2  35238  isrngohom  35245  idlval  35293  isidl  35294  igenval  35341  scottexf  35448  cnvepresex  35593  renegclALT  36101  ldualfvadd  36266  cmtfvalN  36348  cvrfval  36406  cdleme31fv  37528  cdlemk40  38055  cdlemk56  38109  dibopelvalN  38281  dibopelval2  38283  dibelval3  38285  diblsmopel  38309  cdlemn11a  38345  dihopelvalcpre  38386  dihpN  38474  hlhilsca  39073  hlhilip  39086  prjspval  39260  mapfzcons2  39323  jm2.23  39600  jm2.27dlem2  39614  jm2.27dlem4  39616  rmydioph  39618  rmxdioph  39620  expdiophlem2  39626  expdioph  39627  aomclem6  39666  pwslnmlem0  39698  frlmpwfi  39705  mncn0  39746  aaitgo  39769  arearect  39829  areaquad  39830  comptiunov2i  40058  frege110  40326  frege133  40349  scottex2  40588  radcnvrat  40653  uzmptshftfval  40685  dvradcnv2  40686  binomcxplemdvbinom  40692  binomcxplemcvg  40693  binomcxplemnotnn0  40695  rfcnpre1  41283  fcnre  41289  refsumcn  41294  refsum2cnlem1  41301  unirnmapsn  41484  infxrpnf  41728  iocopn  41803  icoopn  41808  mccl  41886  clim1fr1  41889  islptre  41907  sumnnodd  41918  lptre2pt  41928  limclner  41939  limclr  41943  expfac  41945  0cnf  42167  icccncfext  42177  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  itgsin0pilem1  42242  iblempty  42257  itgvol0  42260  stoweidlem47  42339  stoweidlem53  42345  stoweidlem57  42349  stoweidlem59  42351  wallispilem3  42359  wallispilem4  42360  wallispilem5  42361  wallispi  42362  stirlinglem1  42366  stirlinglem8  42373  stirlinglem12  42377  stirlinglem13  42378  stirlinglem14  42379  stirlinglem15  42380  dirkerper  42388  dirkercncflem2  42396  fourierdlem16  42415  fourierdlem21  42420  fourierdlem22  42421  fourierdlem36  42435  fourierdlem42  42441  fourierdlem71  42469  fourierdlem83  42481  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  fourierdlem112  42510  fourierdlem114  42512  sqwvfoura  42520  sqwvfourb  42521  fourierswlem  42522  fouriersw  42523  etransclem48  42574  salexct3  42632  salgencntex  42633  salgensscntex  42634  iooborel  42641  bor1sal  42645  gsumge0cl  42660  sge0tsms  42669  sge0isum  42716  nnfoctbdjlem  42744  isomenndlem  42819  mbfresmf  43023  incsmflem  43025  incsmf  43026  smfmbfcex  43043  decsmflem  43049  decsmf  43050  smflimlem1  43054  smfpimbor1lem2  43081  smf2id  43083  smfco  43084  smfpimcclem  43088  sprsymrelfolem1  43661  sprbisymrel  43668  fmtno0prm  43727  fmtno1prm  43728  fmtno2prm  43729  fmtno3prm  43731  fmtno4prm  43744  m2prm  43760  m3prm  43761  m5prm  43768  m7prm  43771  lighneallem4a  43780  0evenALTV  43860  1oddALTV  43862  2evenALTV  43864  6even  43883  7odd  43884  8even  43885  9gbo  43946  strisomgrop  44012  ushrisomgr  44013  uspgrex  44032  issubmgm2  44064  lmod1zrnlvec  44556  zlmodzxzldeplem1  44562  zlmodzxzldeplem3  44564  zlmodzxzldeplem4  44565  zlmodzxzldep  44566  ldepsnlinclem1  44567  ldepsnlinclem2  44568  blennn0elnn  44644  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687  rrx2line  44734  rrx2linesl  44737  spheres  44740  2sphere  44743  2sphere0  44744  line2x  44748  line2y  44749