Theorem eqeltri 2840

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

Syntax hints:   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eqeltrri  2841  3eltr4i  2857  intab  5002  axrep6g  5311  unisn2  5330  inex2  5336  vpwex  5395  ord3ex  5405  zfpair  5439  vsnex  5449  opex  5484  otex  5485  uniopel  5535  elvvuni  5776  isarep2  6669  fvex  6933  fvexi  6934  riotaex  7408  ovexi  7482  tpex  7781  oprabex  8017  oprabrexex2  8019  mpoexw  8119  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  tfrlem16  8449  1oex  8532  2oex  8533  1on  8534  1onOLD  8535  2on  8536  2onOLD  8537  3on  8540  4on  8541  2oexOLD  8543  oesuclem  8581  oecl  8593  o2p2e4  8597  nnecl  8669  1onnALT  8697  2onnALT  8699  3onn  8700  4onn  8701  mapsnf1o2  8952  sbthlem10  9158  cnvfi  9243  fnfi  9244  nnunifi  9355  imafiOLD  9382  pwfi  9385  xpfiOLD  9387  prfiALT  9392  tpfi  9393  pwfiOLD  9417  fczfsuppd  9455  cantnfvalf  9734  oemapwe  9763  cantnffval2  9764  cnfcom3clem  9774  ssttrcl  9784  r1fin  9842  hta  9966  infxpenlem  10082  alephon  10138  alephfplem1  10173  dfac5lem4  10195  dfac5lem5  10196  dfac5lem4OLD  10197  kmlem10  10229  fin1a2lem10  10478  fin1a2lem12  10480  hsmexlem9  10494  axcc2lem  10505  domtriomlem  10511  axdc2lem  10517  axcclem  10526  brdom7disj  10600  brdom6disj  10601  iundom2g  10609  konigthlem  10637  canthwelem  10719  wunex2  10807  wunex3  10810  1nq  10997  1pr  11084  nrex1  11133  axcnex  11216  ax1cn  11218  pnfex  11343  mnfxr  11347  inelr  12283  cju  12289  nnexALT  12295  2nn  12366  2re  12367  2cn  12368  3nn  12372  3re  12373  3cn  12374  4nn  12376  4re  12377  4cn  12378  5nn  12379  5re  12380  5cn  12381  6nn  12382  6re  12383  6cn  12384  7nn  12385  7re  12386  7cn  12387  8nn  12388  8re  12389  8cn  12390  9nn  12391  9re  12392  9cn  12393  nn0ex  12559  zexALT  12659  nneo  12727  zeo  12729  deccl  12773  10re  12777  decnncl  12778  numnncl2  12781  decnncl2  12782  numsucc  12798  numma2c  12804  numadd  12805  numaddc  12806  nummul1c  12807  nummul2c  12808  decmul1  12822  qexALT  13029  xrex  13052  xnegex  13270  xnegcl  13275  ixxssxr  13419  fz0to4untppr  13687  fz0to5un2tp  13688  om2uzuzi  14000  ltweuz  14012  axdc4uzlem  14034  seqex  14054  seqexw  14068  m1expcl2  14136  faccl  14332  facwordi  14338  faclbnd2  14340  bccl  14371  hashen1  14419  hashrabrsn  14421  hashunlei  14474  hashpw  14485  tpf1o  14550  s1cli  14653  ccat2s1p1  14677  cats1un  14769  revs1  14813  cshwsexa  14872  cshwsexaOLD  14873  cats1cli  14906  cats1fvn  14907  crre  15163  remim  15166  climmpt  15617  sumex  15736  supcvg  15904  geo2lim  15923  prodex  15953  bpoly4  16107  ere  16137  eftlub  16157  efsep  16158  tan0  16199  ef01bndlem  16232  nn0o  16431  divalglem5  16445  divalglem9  16449  sadcf  16499  smupf  16524  crth  16825  phimullem  16826  pczpre  16894  pockthi  16954  prmreclem2  16964  igz  16981  0ramcl  17070  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  strle1  17205  ndxarg  17243  basendxnn  17268  basendxnnOLD  17269  plusgndxnn  17339  tsetndxnn  17413  plendxnn  17427  dsndxnn  17446  unifndxnn  17456  prdsbasex  17510  prdsds  17524  yonedalem3  18350  isposix  18395  isposixOLD  18396  plusffval  18684  issubmgm2  18741  efmnd1hash  18927  efmnd2hash  18929  smndex1bas  18941  smndex1sgrp  18943  smndex1mnd  18945  smndex1id  18946  smndex2dbas  18949  smndex2hbas  18951  grpsubfval  19023  mulgfval  19109  symg1hash  19431  symg2hash  19433  symgvalstruct  19438  symgvalstructOLD  19439  symgfisg  19510  psgnsn  19562  psgnprfval1  19564  odfval  19574  sylow2alem2  19660  efgsval2  19775  efgsp1  19779  pgpfaclem1  20125  dvdsrval  20387  isirred  20445  scaffval  20900  cnfldex  21390  xrsex  21418  pzriprnglem4  21518  pzriprnglem5  21519  pzriprnglem6  21520  pzriprng1ALT  21530  zlmlemOLD  21551  znle  21574  znidomb  21603  cnmsgnsubg  21618  refld  21660  ipffval  21689  psrbag0  22109  psrbagsn  22110  psr1baslem  22207  mat1dimbas  22499  mat1dimscm  22502  mat1f1o  22505  mat1rhmelval  22507  m2detleib  22658  pmatcoe1fsupp  22728  indistopon  23029  iccordt  23243  conncompid  23460  ptbasfi  23610  ptcmpfi  23842  ustfn  24231  ust0  24249  ustn0  24250  tmslem  24515  tmslemOLD  24516  nmfval  24622  tnglemOLD  24675  cnbl0  24815  cnopn  24828  remet  24831  re2ndc  24842  zcld  24854  icccmp  24866  xrge0gsumle  24874  xrge0tsms  24875  xmetdcn  24879  divcnOLD  24909  divcn  24911  expcn  24915  expcnOLD  24917  iiconn  24932  idcncf  24963  cnmpopc  24974  cnrehmeo  25003  cnrehmeoOLD  25004  cnheiborlem  25005  rellycmp  25008  bndth  25009  evth2  25011  cnrlmod  25195  cnrlvec  25196  cncmet  25375  ishl2  25423  ehleudis  25471  ehleudisval  25472  finiunmbl  25598  ioombl1lem4  25615  vitalilem4  25665  vitalilem5  25666  ismbf2d  25694  mbfimaopnlem  25709  mbfi1fseqlem6  25775  itgex  25825  bddmulibl  25894  ditgex  25907  recnperf  25960  dvcnvrelem2  26077  ftc1  26103  mdegcl  26128  plyeq0lem  26269  aaliou3lem4  26406  dvradcnv  26482  sincn  26506  coscn  26507  tanabsge  26566  circsubm  26613  reloggim  26659  logcn  26707  dvloglem  26708  logdmopn  26709  dvlog2  26713  2irrexpq  26791  cxpcn  26805  cxpcnOLD  26806  cxpcn3  26809  resqrtcn  26810  2logb9irrALT  26859  2irrexpqALT  26861  atanrecl  26972  atan1  26989  atansopn  26993  birthdaylem1  27012  birthday  27015  emcllem4  27060  emcllem6  27062  lgamgulmlem6  27095  basellem6  27147  ppiublem1  27264  bposlem6  27351  bposlem8  27353  lgslem4  27362  lgsdir2lem2  27388  selberglem1  27607  selberglem3  27609  selberg  27610  selbergs  27636  qdrng  27682  0sno  27889  1sno  27890  lrrecse  27993  precsexlem11  28259  seqsex  28309  nnsex  28341  n0sbday  28372  n0subs  28378  n0p1nns  28379  dfnns2  28380  zsex  28384  zs12ex  28440  edgfndxnn  29025  structvtxvallem  29055  usgrexmpllem  29295  usgrexmpl  29298  uhgrspan1  29338  upgrres  29341  umgrres  29342  usgrres  29343  upgrres1  29348  umgrres1  29349  usgrres1  29350  fusgrfis  29365  cusgrres  29484  vtxdlfgrval  29521  vtxdusgr0edgnelALT  29532  umgr2v2e  29561  vtxdginducedm1lem1  29575  vtxdginducedm1fi  29580  finsumvtxdg2ssteplem4  29584  pthdlem1  29802  crctcshlem3  29852  2wlkd  29969  2wlkond  29970  2trlond  29972  2pthd  29973  2pthond  29975  umgr2adedgwlkonALT  29980  0pth  30157  wlk2v2e  30189  3wlkd  30202  3trlond  30205  3pthd  30206  3pthond  30207  3spthond  30209  eupthvdres  30267  eulerpathpr  30272  konigsbergumgr  30283  konigsberglem5  30288  konigsberg  30289  ex-lcm  30490  isvciOLD  30612  isnvi  30645  blocni  30837  hmoval  30842  cncph  30851  ipasslem7  30868  siilem2  30884  normlem2  31143  normlem3  31144  normlem6  31147  h0elch  31287  hhssabloilem  31293  hhsssh  31301  spansnji  31678  nonbooli  31683  3oalem5  31698  3oalem6  31699  3oai  31700  mayetes3i  31761  nmcexi  32058  nmbdfnlb  32082  rnelshi  32091  cnlnadjlem5  32103  pjbdlni  32181  golem2  32304  goeqi  32305  dp2clq  32845  rpdp2cl  32846  rpdp2cl2  32847  dpmul100  32861  rpdpcl  32867  chnub  32984  xrge0tsmsd  33041  pmtrto1cl  33092  psgnfzto1stlem  33093  fzto1st  33096  psgnfzto1st  33098  nn0omnd  33338  xrge0slmod  33341  qusima  33401  prmidl0  33443  fply1  33549  ply1degltdimlem  33635  ccfldextdgrr  33682  algextdeglem8  33715  constrfin  33736  2sqr3minply  33738  circtopn  33783  circcn  33784  zarcmplem  33827  tpr2tp  33850  tpr2rico  33858  ordtprsval  33864  ordtprsuni  33865  ordtrestNEW  33867  ordtrest2NEWlem  33868  ordtrest2NEW  33869  ordtconnlem1  33870  mndpluscn  33872  xrge0pluscn  33886  xrge0mulc1cn  33887  xrge0haus  33890  lmlimxrge0  33894  lmxrge0  33898  qqhcn  33937  qqhucn  33938  esumex  33993  esumcst  34027  hasheuni  34049  esumcvg  34050  prsiga  34095  brsiga  34147  mbfmcnt  34233  sxbrsigalem3  34237  dya2iocuni  34248  dya2iocucvr  34249  sxbrsigalem1  34250  sxbrsiga  34255  eulerpartlemt  34336  fibp1  34366  coinflipprob  34444  coinfliprv  34447  ccatmulgnn0dir  34519  signswplusg  34532  hgt750lem2  34629  hgt750leme  34635  bnj105  34700  bnj918  34742  bnj95  34840  bnj852  34897  bnj865  34899  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  35697  altopex  35924  colinearex  36024  ssoninhaus  36414  cnndvlem2  36504  bj-prex  37006  bj-prfromadj  37011  bj-pinftyccb  37187  taupi  37289  isbasisrelowl  37324  relowlpssretop  37330  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  dvasin  37664  dvacos  37665  areacirc  37673  upixp  37689  fdc  37705  lmclim2  37718  cncfres  37725  heibor1lem  37769  rrnval  37787  rrnmet  37789  reheibor  37799  isdrngo2  37918  isrngohom  37925  idlval  37973  isidl  37974  igenval  38021  scottexf  38128  cnvepresex  38290  renegclALT  38919  ldualfvadd  39084  cmtfvalN  39166  cvrfval  39224  cdleme31fv  40347  cdlemk40  40874  cdlemk56  40928  dibopelvalN  41100  dibopelval2  41102  dibelval3  41104  diblsmopel  41128  cdlemn11a  41164  dihopelvalcpre  41205  dihpN  41293  hlhilsca  41892  hlhilip  41909  3factsumint1  41978  lcmineqlem23  42008  aks4d1p1p6  42030  aks4d1p1p5  42032  aks6d1c6isolem2  42132  itrere  42307  acos1half  42340  sn-0tie0  42415  sn-itrere  42444  sn-retire  42445  prjspval  42558  flt4lem5e  42611  sn-isghm  42628  mapfzcons2  42675  jm2.23  42953  jm2.27dlem2  42967  jm2.27dlem4  42969  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  aomclem6  43016  pwslnmlem0  43048  frlmpwfi  43055  mncn0  43096  aaitgo  43119  arearect  43176  areaquad  43177  omcl3g  43296  comptiunov2i  43668  frege110  43935  frege133  43958  scottex2  44214  radcnvrat  44283  uzmptshftfval  44315  dvradcnv2  44316  binomcxplemdvbinom  44322  binomcxplemcvg  44323  binomcxplemnotnn0  44325  rfcnpre1  44919  fcnre  44925  refsumcn  44930  refsum2cnlem1  44937  unirnmapsn  45121  infxrpnf  45361  iocopn  45438  icoopn  45443  mccl  45519  clim1fr1  45522  islptre  45540  sumnnodd  45551  lptre2pt  45561  limclner  45572  limclr  45576  expfac  45578  0cnf  45798  icccncfext  45808  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  itgsin0pilem1  45871  iblempty  45886  itgvol0  45889  stoweidlem47  45968  stoweidlem53  45974  stoweidlem57  45978  stoweidlem59  45980  wallispilem3  45988  wallispilem4  45989  wallispilem5  45990  wallispi  45991  stirlinglem1  45995  stirlinglem8  46002  stirlinglem12  46006  stirlinglem13  46007  stirlinglem14  46008  stirlinglem15  46009  dirkerper  46017  dirkercncflem2  46025  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem36  46064  fourierdlem42  46070  fourierdlem71  46098  fourierdlem83  46110  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem114  46141  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  etransclem48  46203  salexct3  46263  salgencntex  46264  salgensscntex  46265  iooborel  46272  bor1sal  46276  gsumge0cl  46292  sge0tsms  46301  sge0isum  46348  nnfoctbdjlem  46376  isomenndlem  46451  mbfresmf  46660  incsmflem  46662  incsmf  46663  smfmbfcex  46681  decsmflem  46687  decsmf  46688  smflimlem1  46692  smfpimbor1lem2  46720  smf2id  46722  smfco  46723  smfpimcclem  46728  tworepnotupword  46805  sprsymrelfolem1  47366  sprbisymrel  47373  fmtno0prm  47432  fmtno1prm  47433  fmtno2prm  47434  fmtno3prm  47436  fmtno4prm  47449  m2prm  47465  m3prm  47466  m5prm  47472  m7prm  47474  lighneallem4a  47482  0evenALTV  47562  1oddALTV  47564  2evenALTV  47566  6even  47585  7odd  47586  8even  47587  9gbo  47648  opstrgric  47779  ushggricedg  47780  grtri  47791  usgrexmpl1  47837  usgrexmpl1vtx  47838  usgrexmpl1edg  47839  usgrexmpl2  47842  usgrexmpl2vtx  47843  usgrexmpl2edg  47844  uspgrex  47873  lmod1zrnlvec  48223  zlmodzxzldeplem1  48229  zlmodzxzldeplem3  48231  zlmodzxzldeplem4  48232  zlmodzxzldep  48233  ldepsnlinclem1  48234  ldepsnlinclem2  48235  blennn0elnn  48311  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  itcovalpclem2  48405  itcovalt2lem2  48410  ackval42  48430  rrx2line  48474  rrx2linesl  48477  spheres  48480  2sphere  48483  2sphere0  48484  line2x  48488  line2y  48489  functhinclem1  48708  prsthinc  48721