Theorem eqeltri 2830

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 2825	. 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 2707

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

This theorem is referenced by:  eqeltrri  2831  3eltr4i  2847  intab  4954  axrep6g  5260  unisn2  5282  inex2  5288  vpwex  5347  ord3ex  5357  zfpair  5391  vsnex  5404  opex  5439  otex  5440  uniopel  5491  elvvuni  5731  isarep2  6627  fvex  6888  fvexi  6889  riotaex  7364  ovexi  7437  tpex  7738  oprabex  7973  oprabrexex2  7975  mpoexw  8075  mptmpoopabbrd  8077  mptmpoopabbrdOLD  8078  tfrlem16  8405  1oex  8488  2oex  8489  1on  8490  1onOLD  8491  2on  8492  2onOLD  8493  3on  8496  4on  8497  oesuclem  8535  oecl  8547  o2p2e4  8551  nnecl  8623  1onnALT  8651  2onnALT  8653  3onn  8654  4onn  8655  mapsnf1o2  8906  sbthlem10  9104  cnvfi  9188  fnfi  9190  nnunifi  9297  imafiOLD  9324  pwfi  9327  xpfiOLD  9329  prfiALT  9334  tpfi  9335  fczfsuppd  9396  cantnfvalf  9677  oemapwe  9706  cantnffval2  9707  cnfcom3clem  9717  ssttrcl  9727  r1fin  9785  hta  9909  infxpenlem  10025  alephon  10081  alephfplem1  10116  dfac5lem4  10138  dfac5lem5  10139  dfac5lem4OLD  10140  kmlem10  10172  fin1a2lem10  10421  fin1a2lem12  10423  hsmexlem9  10437  axcc2lem  10448  domtriomlem  10454  axdc2lem  10460  axcclem  10469  brdom7disj  10543  brdom6disj  10544  iundom2g  10552  konigthlem  10580  canthwelem  10662  wunex2  10750  wunex3  10753  1nq  10940  1pr  11027  nrex1  11076  axcnex  11159  ax1cn  11161  pnfex  11286  mnfxr  11290  inelr  12228  cju  12234  nnexALT  12240  2nn  12311  2re  12312  2cn  12313  3nn  12317  3re  12318  3cn  12319  4nn  12321  4re  12322  4cn  12323  5nn  12324  5re  12325  5cn  12326  6nn  12327  6re  12328  6cn  12329  7nn  12330  7re  12331  7cn  12332  8nn  12333  8re  12334  8cn  12335  9nn  12336  9re  12337  9cn  12338  nn0ex  12505  zexALT  12606  nneo  12675  zeo  12677  deccl  12721  10re  12725  decnncl  12726  numnncl2  12729  decnncl2  12730  numsucc  12746  numma2c  12752  numadd  12753  numaddc  12754  nummul1c  12755  nummul2c  12756  decmul1  12770  qexALT  12978  xrex  13001  xnegex  13222  xnegcl  13227  ixxssxr  13372  fz0to4untppr  13645  fz0to5un2tp  13646  om2uzuzi  13965  ltweuz  13977  axdc4uzlem  13999  seqex  14019  seqexw  14033  m1expcl2  14101  faccl  14299  facwordi  14305  faclbnd2  14307  bccl  14338  hashen1  14386  hashrabrsn  14388  hashunlei  14441  hashpw  14452  tpf1o  14517  s1cli  14621  ccat2s1p1  14645  cats1un  14737  revs1  14781  cshwsexa  14840  cshwsexaOLD  14841  cats1cli  14874  cats1fvn  14875  crre  15131  remim  15134  climmpt  15585  sumex  15702  supcvg  15870  geo2lim  15889  prodex  15919  bpoly4  16073  ere  16103  eftlub  16125  efsep  16126  tan0  16167  ef01bndlem  16200  nn0o  16400  divalglem5  16414  divalglem9  16418  sadcf  16470  smupf  16495  crth  16795  phimullem  16796  pczpre  16865  pockthi  16925  prmreclem2  16935  igz  16952  0ramcl  17041  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  1259prm  17153  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  4001prm  17162  strle1  17175  ndxarg  17213  basendxnn  17236  plusgndxnn  17297  tsetndxnn  17366  plendxnn  17380  dsndxnn  17399  unifndxnn  17409  prdsbasex  17462  prdsds  17476  yonedalem3  18290  isposix  18334  plusffval  18622  issubmgm2  18679  efmnd1hash  18868  efmnd2hash  18870  smndex1bas  18882  smndex1sgrp  18884  smndex1mnd  18886  smndex1id  18887  smndex2dbas  18890  smndex2hbas  18892  grpsubfval  18964  mulgfval  19050  symg1hash  19369  symg2hash  19371  symgvalstruct  19376  symgfisg  19447  psgnsn  19499  psgnprfval1  19501  odfval  19511  sylow2alem2  19597  efgsval2  19712  efgsp1  19716  pgpfaclem1  20062  dvdsrval  20319  isirred  20377  scaffval  20835  cnfldex  21316  xrsex  21343  pzriprnglem4  21443  pzriprnglem5  21444  pzriprnglem6  21445  pzriprng1ALT  21455  znle  21495  znidomb  21520  cnmsgnsubg  21535  refld  21577  ipffval  21606  psrbag0  22018  psrbagsn  22019  psr1baslem  22118  mat1dimbas  22408  mat1dimscm  22411  mat1f1o  22414  mat1rhmelval  22416  m2detleib  22567  pmatcoe1fsupp  22637  indistopon  22937  iccordt  23150  conncompid  23367  ptbasfi  23517  ptcmpfi  23749  ustfn  24138  ust0  24156  ustn0  24157  tmslem  24419  nmfval  24525  cnbl0  24710  cnopn  24723  remet  24727  re2ndc  24738  zcld  24751  icccmp  24763  xrge0gsumle  24771  xrge0tsms  24772  xmetdcn  24776  divcnOLD  24806  divcn  24808  expcn  24812  expcnOLD  24814  iiconn  24829  idcncf  24860  cnmpopc  24871  cnrehmeo  24900  cnrehmeoOLD  24901  cnheiborlem  24902  rellycmp  24905  bndth  24906  evth2  24908  cnrlmod  25092  cnrlvec  25093  cncmet  25272  ishl2  25320  ehleudis  25368  ehleudisval  25369  finiunmbl  25495  ioombl1lem4  25512  vitalilem4  25562  vitalilem5  25563  ismbf2d  25591  mbfimaopnlem  25606  mbfi1fseqlem6  25671  itgex  25721  bddmulibl  25790  ditgex  25803  recnperf  25856  dvcnvrelem2  25973  ftc1  25999  mdegcl  26024  plyeq0lem  26165  aaliou3lem4  26304  dvradcnv  26380  sincn  26404  coscn  26405  tanabsge  26465  circsubm  26512  reloggim  26558  logcn  26606  dvloglem  26607  logdmopn  26608  dvlog2  26612  2irrexpq  26690  cxpcn  26704  cxpcnOLD  26705  cxpcn3  26708  resqrtcn  26709  2logb9irrALT  26758  2irrexpqALT  26760  atanrecl  26871  atan1  26888  atansopn  26892  birthdaylem1  26911  birthday  26914  emcllem4  26959  emcllem6  26961  lgamgulmlem6  26994  basellem6  27046  ppiublem1  27163  bposlem6  27250  bposlem8  27252  lgslem4  27261  lgsdir2lem2  27287  selberglem1  27506  selberglem3  27508  selberg  27509  selbergs  27535  qdrng  27581  0sno  27788  1sno  27789  lrrecse  27892  precsexlem11  28158  seqsex  28208  nnsex  28240  n0sbday  28271  n0subs  28277  n0p1nns  28278  dfnns2  28279  zsex  28283  zs12ex  28339  edgfndxnn  28917  structvtxvallem  28945  usgrexmpllem  29185  usgrexmpl  29188  uhgrspan1  29228  upgrres  29231  umgrres  29232  usgrres  29233  upgrres1  29238  umgrres1  29239  usgrres1  29240  fusgrfis  29255  cusgrres  29374  vtxdlfgrval  29411  vtxdusgr0edgnelALT  29422  umgr2v2e  29451  vtxdginducedm1lem1  29465  vtxdginducedm1fi  29470  finsumvtxdg2ssteplem4  29474  pthdlem1  29694  crctcshlem3  29747  2wlkd  29864  2wlkond  29865  2trlond  29867  2pthd  29868  2pthond  29870  umgr2adedgwlkonALT  29875  0pth  30052  wlk2v2e  30084  3wlkd  30097  3trlond  30100  3pthd  30101  3pthond  30102  3spthond  30104  eupthvdres  30162  eulerpathpr  30167  konigsbergumgr  30178  konigsberglem5  30183  konigsberg  30184  ex-lcm  30385  isvciOLD  30507  isnvi  30540  blocni  30732  hmoval  30737  cncph  30746  ipasslem7  30763  siilem2  30779  normlem2  31038  normlem3  31039  normlem6  31042  h0elch  31182  hhssabloilem  31188  hhsssh  31196  spansnji  31573  nonbooli  31578  3oalem5  31593  3oalem6  31594  3oai  31595  mayetes3i  31656  nmcexi  31953  nmbdfnlb  31977  rnelshi  31986  cnlnadjlem5  31998  pjbdlni  32076  golem2  32199  goeqi  32200  dp2clq  32801  rpdp2cl  32802  rpdp2cl2  32803  dpmul100  32817  rpdpcl  32823  chnub  32938  xrge0tsmsd  33002  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1st  33060  psgnfzto1st  33062  nn0omnd  33306  xrge0slmod  33309  qusima  33369  prmidl0  33411  fply1  33517  ply1degltdimlem  33608  ccfldextdgrr  33659  algextdeglem8  33704  constrfin  33726  2sqr3minply  33760  2sqr3nconstr  33761  cos9thpiminplylem4  33765  cos9thpiminplylem5  33766  circtopn  33814  circcn  33815  zarcmplem  33858  tpr2tp  33881  tpr2rico  33889  ordtprsval  33895  ordtprsuni  33896  ordtrestNEW  33898  ordtrest2NEWlem  33899  ordtrest2NEW  33900  ordtconnlem1  33901  mndpluscn  33903  xrge0pluscn  33917  xrge0mulc1cn  33918  xrge0haus  33921  lmlimxrge0  33925  lmxrge0  33929  qqhcn  33968  qqhucn  33969  esumex  34006  esumcst  34040  hasheuni  34062  esumcvg  34063  prsiga  34108  brsiga  34160  mbfmcnt  34246  sxbrsigalem3  34250  dya2iocuni  34261  dya2iocucvr  34262  sxbrsigalem1  34263  sxbrsiga  34268  eulerpartlemt  34349  fibp1  34379  coinflipprob  34458  coinfliprv  34461  ccatmulgnn0dir  34520  signswplusg  34533  hgt750lem2  34630  hgt750leme  34636  bnj105  34701  bnj918  34743  bnj95  34841  bnj852  34898  bnj865  34900  subfacp1lem1  35147  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  kur14lem7  35180  iisconn  35220  iillysconn  35221  cvmliftlem5  35257  cvmliftlem8  35260  cvmliftlem10  35262  cvmlift2lem9  35279  satfv0  35326  goalrlem  35364  goalr  35365  satffunlem2lem2  35374  circum  35642  iexpire  35698  altopex  35924  colinearex  36024  ssoninhaus  36412  cnndvlem2  36502  bj-prex  37004  bj-prfromadj  37009  bj-pinftyccb  37185  taupi  37287  isbasisrelowl  37322  relowlpssretop  37328  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  dvasin  37674  dvacos  37675  areacirc  37683  upixp  37699  fdc  37715  lmclim2  37728  cncfres  37735  heibor1lem  37779  rrnval  37797  rrnmet  37799  reheibor  37809  isdrngo2  37928  isrngohom  37935  idlval  37983  isidl  37984  igenval  38031  scottexf  38138  cnvepresex  38298  renegclALT  38927  ldualfvadd  39092  cmtfvalN  39174  cvrfval  39232  cdleme31fv  40355  cdlemk40  40882  cdlemk56  40936  dibopelvalN  41108  dibopelval2  41110  dibelval3  41112  diblsmopel  41136  cdlemn11a  41172  dihopelvalcpre  41213  dihpN  41301  hlhilsca  41900  hlhilip  41913  3factsumint1  41980  lcmineqlem23  42010  aks4d1p1p6  42032  aks4d1p1p5  42034  aks6d1c6isolem2  42134  itrere  42314  acos1half  42348  redvmptabs  42350  readvrec2  42351  sn-0tie0  42429  sn-itrere  42458  sn-retire  42459  prjspval  42573  flt4lem5e  42626  sn-isghm  42643  mapfzcons2  42689  jm2.23  42967  jm2.27dlem2  42981  jm2.27dlem4  42983  rmydioph  42985  rmxdioph  42987  expdiophlem2  42993  expdioph  42994  aomclem6  43030  pwslnmlem0  43062  frlmpwfi  43069  mncn0  43110  aaitgo  43133  arearect  43186  areaquad  43187  omcl3g  43305  comptiunov2i  43677  frege110  43944  frege133  43967  scottex2  44217  radcnvrat  44286  uzmptshftfval  44318  dvradcnv2  44319  binomcxplemdvbinom  44325  binomcxplemcvg  44326  binomcxplemnotnn0  44328  permaxinf2lem  44985  rfcnpre1  44991  fcnre  44997  refsumcn  45002  refsum2cnlem1  45009  unirnmapsn  45186  infxrpnf  45421  iocopn  45497  icoopn  45502  mccl  45575  clim1fr1  45578  islptre  45596  sumnnodd  45607  lptre2pt  45617  limclner  45628  limclr  45632  expfac  45634  0cnf  45854  icccncfext  45864  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  itgsin0pilem1  45927  iblempty  45942  itgvol0  45945  stoweidlem47  46024  stoweidlem53  46030  stoweidlem57  46034  stoweidlem59  46036  wallispilem3  46044  wallispilem4  46045  wallispilem5  46046  wallispi  46047  stirlinglem1  46051  stirlinglem8  46058  stirlinglem12  46062  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  dirkerper  46073  dirkercncflem2  46081  fourierdlem16  46100  fourierdlem21  46105  fourierdlem22  46106  fourierdlem36  46120  fourierdlem42  46126  fourierdlem71  46154  fourierdlem83  46166  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem114  46197  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  etransclem48  46259  salexct3  46319  salgencntex  46320  salgensscntex  46321  iooborel  46328  bor1sal  46332  gsumge0cl  46348  sge0tsms  46357  sge0isum  46404  nnfoctbdjlem  46432  isomenndlem  46507  mbfresmf  46716  incsmflem  46718  incsmf  46719  smfmbfcex  46737  decsmflem  46743  decsmf  46744  smflimlem1  46748  smfpimbor1lem2  46776  smf2id  46778  smfco  46779  smfpimcclem  46784  tworepnotupword  46863  lambert0  46867  sprsymrelfolem1  47454  sprbisymrel  47461  fmtno0prm  47520  fmtno1prm  47521  fmtno2prm  47522  fmtno3prm  47524  fmtno4prm  47537  m2prm  47553  m3prm  47554  m5prm  47560  m7prm  47562  lighneallem4a  47570  0evenALTV  47650  1oddALTV  47652  2evenALTV  47654  6even  47673  7odd  47674  8even  47675  9gbo  47736  opstrgric  47887  ushggricedg  47888  grtri  47900  usgrexmpl1  47974  usgrexmpl1vtx  47975  usgrexmpl1edg  47976  usgrexmpl2  47979  usgrexmpl2vtx  47980  usgrexmpl2edg  47981  gpgprismgr4cycllem5  48046  uspgrex  48073  lmod1zrnlvec  48418  zlmodzxzldeplem1  48424  zlmodzxzldeplem3  48426  zlmodzxzldeplem4  48427  zlmodzxzldep  48428  ldepsnlinclem1  48429  ldepsnlinclem2  48430  blennn0elnn  48505  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  itcovalpclem2  48599  itcovalt2lem2  48604  ackval42  48624  rrx2line  48668  rrx2linesl  48671  spheres  48674  2sphere  48677  2sphere0  48678  line2x  48682  line2y  48683  resipos  48897  functhinclem1  49278  prsthinc  49298  setc1oterm  49324  funcsetc1ocl  49329  funcsetc1o  49330  isinito2lem  49331  isinito3  49333  functermc2  49342  incat  49426  setc1onsubc  49427