Theorem eqeltri 2859

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838

This theorem is used by:  eqeltrri  2860  3eltr4i  2876  intab  4940  axrep6g  5245  unisn2  5268  inex2  5281  vpwex  5342  ord3ex  5352  zfpair  5386  vsnex  5396  snex  5400  opex  5435  opexOLD  5436  otex  5437  uniopel  5492  elvvuni  5732  isarep2  6637  fvex  6906  fvexi  6907  riotaex  7388  ovexi  7461  tpex  7769  oprabex  7995  oprabrexex2  7997  mpoexw  8099  mptmpoopabbrd  8102  tfrlem16  8412  1oex  8497  2oex  8499  1on  8500  2on  8501  3on  8504  4on  8505  oesuclem  8544  oecl  8556  o2p2e4  8560  nnecl  8633  1onnALT  8661  2onnALT  8663  3onn  8664  4onn  8665  mapsnf1o2  8933  sbthlem10  9126  cnvfi  9202  fnfi  9204  nnunifi  9294  pwfi  9321  prfiALT  9327  tpfi  9328  fczfsuppd  9388  cantnfvalf  9676  oemapwe  9705  cantnffval2  9706  cnfcom3clem  9716  ssttrcl  9726  r1fin  9790  scottex  9943  scottex2OLD  9956  hta  9972  htaOLD  9973  infxpenlem  10102  alephon  10158  alephfplem1  10193  dfac5lem4  10215  dfac5lem5  10216  kmlem10  10248  fin1a2lem10  10497  fin1a2lem12  10499  hsmexlem9  10513  axcc2lem  10524  domtriomlem  10530  axdc2lem  10536  axcclem  10545  brdom7disj  10620  brdom6disj  10621  iundom2g  10634  konigthlem  10663  canthwelem  10745  wunex2  10833  wunex3  10836  hftsk  10874  1nq  11023  1pr  11110  nrex1  11159  axcnex  11242  ax1cn  11244  pnfex  11372  mnfxr  11376  cju  12326  nnexALT  12347  2nn  12426  2re  12427  2cn  12428  3nn  12432  3re  12433  3cn  12434  4nn  12436  4re  12437  4cn  12438  5nn  12439  5re  12440  5cn  12441  6nn  12442  6re  12443  6cn  12444  7nn  12445  7re  12446  7cn  12447  8nn  12448  8re  12449  8cn  12450  9nn  12451  9re  12452  9cn  12453  nn0ex  12622  zexALT  12723  nneo  12793  zeo  12795  deccl  12839  10re  12847  decnncl  12848  numnncl2  12852  decnncl2  12853  numsucc  12869  numma2c  12875  numadd  12876  numaddc  12877  nummul1c  12878  nummul2c  12879  decmul1  12893  qexALT  13101  xrex  13125  xnegex  13348  xnegcl  13353  ixxssxr  13498  fz0to4untppr  13774  fz0to5un2tp  13775  om2uzuzi  14102  ltweuz  14114  axdc4uzlem  14136  seqex  14156  seqexw  14170  m1expcl2  14238  faccl  14437  facwordi  14443  faclbnd2  14445  bccl  14476  hashen1  14524  hashrabrsn  14526  hashunlei  14580  hashpw  14591  tpf1o  14656  s1cli  14762  ccat2s1p1  14788  cats1un  14881  revs1  14925  cshwsexa  14986  cats1cli  15019  cats1fvn  15020  crre  15293  remim  15296  climmpt  15750  sumex  15867  supcvg  16037  geo2lim  16056  prodex  16086  bpoly4  16237  ere  16267  eftlub  16289  efsep  16290  tan0  16331  ef01bndlem  16364  nn0o  16565  divalglem5  16579  divalglem9  16583  sadcf  16635  smupf  16660  crth  16967  phimullem  16968  pczpre  17037  pockthi  17097  igz  17124  0ramcl  17213  1259lem1  17321  1259lem2  17322  1259lem3  17323  1259lem4  17324  1259lem5  17325  1259prm  17326  2503lem1  17327  2503lem2  17328  2503lem3  17329  2503prm  17330  4001lem1  17331  4001lem2  17332  4001lem3  17333  4001lem4  17334  4001prm  17335  strle1  17348  ndxarg  17386  basendxnn  17409  plusgndxnn  17468  tsetndxnn  17537  plendxnn  17551  dsndxnn  17570  unifndxnn  17580  prdsbasex  17633  prdsds  17647  yonedalem3  18466  isposix  18510  chnub  18808  plusffval  18834  issubmgm2  18904  efmnd1hash  19100  efmnd2hash  19102  smndex1bas  19117  smndex1sgrp  19119  smndex1mnd  19121  smndex1id  19122  smndex2dbas  19125  smndex2hbas  19127  grpsubfval  19206  mulgfval  19291  symg1hash  19616  symg2hash  19618  symgvalstruct  19623  symgfisg  19694  psgnsn  19746  psgnprfval1  19748  odfval  19758  sylow2alem2  19844  efgsval2  19959  efgsp1  19963  pgpfaclem1  20309  dvdsrval  20603  isirred  20661  scaffval  21167  prmidl0  21646  cnfldex  21693  xrsex  21707  pzriprnglem4  21802  pzriprnglem5  21803  pzriprnglem6  21804  pzriprng1ALT  21814  znle  21854  znidomb  21879  cnmsgnsubg  21895  refld  21937  ipffval  21966  psrbag0  22383  psrbagsn  22384  psr1baslem  22515  mat1dimbas  22799  mat1dimscm  22802  mat1f1o  22805  mat1rhmelval  22807  m2detleib  22958  pmatcoe1fsupp  23031  indistopon  23331  iccordt  23544  conncompid  23761  ptbasfi  23912  ptcmpfi  24144  ustfn  24533  ust0  24551  ustn0  24552  tmslem  24813  nmfval  24919  cnbl0  25104  cnopn  25117  remet  25121  re2ndc  25132  zcld  25145  icccmp  25157  xrge0gsumle  25165  xrge0tsms  25166  xmetdcn  25170  divcn  25201  expcn  25205  iiconn  25220  idcncf  25251  cnmpopc  25261  cnrehmeo  25286  cnheiborlem  25287  rellycmp  25290  bndth  25291  evth2  25293  cnrlmod  25476  cnrlvec  25477  cncmet  25655  ishl2  25703  ehleudis  25751  ehleudisval  25752  finiunmbl  25877  ioombl1lem4  25894  vitalilem4  25944  vitalilem5  25945  ismbf2d  25973  mbfimaopnlem  25988  mbfi1fseqlem6  26053  itgex  26103  bddmulibl  26171  ditgex  26184  recnperf  26237  dvcnvrelem2  26350  ftc1  26374  mdegcl  26399  plyeq0lem  26541  iaa  26663  aaliou3lem4  26685  dvradcnv  26760  sincn  26783  coscn  26784  tanabsge  26847  circsubm  26893  reloggim  26939  logcn  26987  dvloglem  26988  logdmopn  26989  dvlog2  26993  2irrexpq  27071  cxpcn  27085  cxpcn3  27088  resqrtcn  27089  2logb9irrALT  27138  2irrexpqALT  27140  atanrecl  27251  atan1  27268  atansopn  27272  birthdaylem1  27291  birthday  27294  emcllem4  27338  emcllem6  27340  lgamgulmlem6  27373  basellem6  27425  ppiublem1  27541  bposlem6  27628  bposlem8  27630  lgslem4  27639  lgsdir2lem2  27665  selberglem1  27884  selberglem3  27886  selberg  27887  selbergs  27913  qdrng  27959  0no  28207  1no  28208  lrrecse  28340  precsexlem11  28615  seqsex  28683  nnsex  28716  n0bday  28750  n0subs  28761  n0p1nns  28769  dfnns2  28770  zsex  28778  bdayfinbndlem1  28865  z12sex  28872  z12shalf  28878  angmgmlem  29407  edgfndxnn  29582  structvtxvallem  29610  usgrexmpllem  29853  usgrexmpl  29856  uhgrspan1  29896  upgrres  29899  umgrres  29900  usgrres  29901  upgrres1  29906  umgrres1  29907  usgrres1  29908  fusgrfis  29923  cusgrres  30041  vtxdlfgrval  30078  vtxdusgr0edgnelALT  30089  umgr2v2e  30118  vtxdginducedm1lem1  30132  vtxdginducedm1fi  30137  finsumvtxdg2ssteplem4  30141  pthdlem1  30364  crctcshlem3  30420  2wlkd  30537  2wlkond  30538  2trlond  30540  2pthd  30541  2pthond  30543  umgr2adedgwlkonALT  30548  0pth  30728  wlk2v2e  30770  3wlkd  30783  3trlond  30786  3pthd  30787  3pthond  30788  3spthond  30790  eupthvdres  30848  eulerpathpr  30853  konigsbergumgr  30864  konigsberglem5  30869  konigsberg  30870  ex-lcm  31071  isvciOLD  31194  isnvi  31227  blocni  31419  hmoval  31424  cncph  31433  ipasslem7  31450  siilem2  31466  normlem2  31725  normlem3  31726  normlem6  31729  h0elch  31869  hhssabloilem  31875  hhsssh  31883  spansnji  32260  nonbooli  32265  3oalem5  32280  3oalem6  32281  3oai  32282  mayetes3i  32343  nmcexi  32640  nmbdfnlb  32664  rnelshi  32673  cnlnadjlem5  32685  pjbdlni  32763  golem2  32886  goeqi  32887  dp2clq  33500  rpdp2cl  33501  rpdp2cl2  33502  dpmul100  33516  rpdpcl  33522  xrge0tsmsd  33687  pmtrto1cl  33713  psgnfzto1stlem  33714  fzto1st  33717  psgnfzto1st  33719  nn0omnd  33958  xrge0slmod  33962  qusima  34012  fply1  34143  extvfvcl  34221  ply1degltdimlem  34307  ccfldextdgrr  34357  algextdeglem8  34409  constrfin  34431  2sqr3minply  34465  2sqr3nconstr  34466  cos9thpiminplylem4  34470  cos9thpiminplylem5  34471  cos9thpinconstrlem2  34475  circtopn  34522  circcn  34523  zarcmplem  34566  tpr2tp  34589  tpr2rico  34597  ordtprsval  34603  ordtprsuni  34604  ordtrestNEW  34606  ordtrest2NEWlem  34607  ordtrest2NEW  34608  ordtconnlem1  34609  mndpluscn  34611  xrge0pluscn  34625  xrge0mulc1cn  34626  xrge0haus  34629  lmlimxrge0  34633  lmxrge0  34637  qqhcn  34676  qqhucn  34677  esumex  34714  esumcst  34748  hasheuni  34770  esumcvg  34771  prsiga  34816  brsiga  34869  mbfmcnt  34953  sxbrsigalem3  34957  dya2iocuni  34968  dya2iocucvr  34969  sxbrsigalem1  34970  sxbrsiga  34975  eulerpartlemt  35056  fibp1  35086  coinflipprob  35165  coinfliprv  35168  ccatmulgnn0dir  35227  signswplusg  35237  hgt750lem2  35334  hgt750leme  35340  bnj105  35408  bnj918  35450  bnj95  35547  bnj852  35604  bnj865  35606  5on  35842  6on  35843  7on  35844  8on  35845  9on  35846  5onn  35847  6onn  35848  7onn  35849  8onn  35850  9onn  35851  fineqvnttrclse  35863  subfacp1lem1  36065  subfacp1lem3  36068  subfacp1lem5  36070  subfacp1lem6  36071  kur14lem7  36098  iisconn  36138  iillysconn  36139  cvmliftlem5  36175  cvmliftlem8  36178  cvmliftlem10  36180  cvmlift2lem9  36197  satfv0  36244  goalrlem  36282  goalr  36283  satffunlem2lem2  36292  circum  36560  iexpire  36627  altopex  36852  colinearex  36952  ssoninhaus  37363  cnndvlem2  37531  bj-prex  38080  bj-prfromadj  38085  bj-pinftyccb  38282  taupi  38384  isbasisrelowl  38421  relowlpssretop  38427  poimirlem29  38707  poimirlem30  38708  poimirlem31  38709  dvasin  38762  dvacos  38763  areacirc  38771  upixp  38803  fdc  38819  lmclim2  38832  cncfres  38839  heibor1lem  38883  rrnval  38901  rrnmet  38903  reheibor  38913  isdrngo2  39032  isrngohom  39039  idlval  39087  isidl  39088  igenval  39135  scottexf  39240  cnvepresex  39408  preex  39564  renegclALT  40160  ldualfvadd  40325  cmtfvalN  40407  cvrfval  40465  cdleme31fv  41587  cdlemk40  42114  cdlemk56  42168  dibopelvalN  42340  dibopelval2  42342  dibelval3  42344  diblsmopel  42368  cdlemn11a  42404  dihopelvalcpre  42445  dihpN  42533  hlhilsca  43132  hlhilip  43145  3factsumint1  43211  lcmineqlem23  43241  aks4d1p1p6  43263  aks4d1p1p5  43265  aks6d1c6isolem2  43365  25or6to4  43396  itrere  43515  acos1half  43549  redvmptabs  43551  readvrec2  43552  sn-0tie0  43655  sn-itrere  43692  sn-retire  43693  prjspval  43771  sn-isghm  43824  mapfzcons2  43870  jm2.23  44143  jm2.27dlem2  44157  jm2.27dlem4  44159  rmydioph  44161  rmxdioph  44163  expdiophlem2  44169  expdioph  44170  aomclem6  44201  pwslnmlem0  44233  frlmpwfi  44240  mncn0  44281  aaitgo  44304  arearect  44357  areaquad  44358  omcl3g  44476  comptiunov2i  44846  frege110  45113  frege133  45136  radcnvrat  45438  uzmptshftfval  45470  dvradcnv2  45471  binomcxplemdvbinom  45477  binomcxplemcvg  45478  binomcxplemnotnn0  45480  permaxinf2lem  46141  rfcnpre1  46175  fcnre  46181  refsumcn  46186  refsum2cnlem1  46193  unirnmapsn  46366  infxrpnf  46595  iocopn  46671  icoopn  46676  mccl  46749  clim1fr1  46752  islptre  46770  sumnnodd  46781  lptre2pt  46789  limclner  46800  limclr  46804  expfac  46806  0cnf  47026  icccncfext  47036  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  itgsin0pilem1  47099  iblempty  47114  itgvol0  47117  stoweidlem47  47196  stoweidlem53  47202  stoweidlem57  47206  stoweidlem59  47208  wallispilem3  47216  wallispilem4  47217  wallispilem5  47218  wallispi  47219  stirlinglem1  47223  stirlinglem8  47230  stirlinglem12  47234  stirlinglem13  47235  stirlinglem14  47236  stirlinglem15  47237  dirkerper  47245  dirkercncflem2  47253  fourierdlem16  47272  fourierdlem21  47277  fourierdlem22  47278  fourierdlem36  47292  fourierdlem42  47298  fourierdlem71  47326  fourierdlem83  47338  fourierdlem102  47357  fourierdlem103  47358  fourierdlem104  47359  fourierdlem111  47366  fourierdlem112  47367  fourierdlem114  47369  sqwvfoura  47377  sqwvfourb  47378  fourierswlem  47379  fouriersw  47380  etransclem48  47431  salexct3  47491  salgencntex  47492  salgensscntex  47493  iooborel  47500  bor1sal  47504  gsumge0cl  47520  sge0tsms  47529  sge0isum  47576  nnfoctbdjlem  47604  isomenndlem  47679  mbfresmf  47888  incsmflem  47890  incsmf  47891  smfmbfcex  47909  decsmflem  47915  decsmf  47916  smflimlem1  47920  smfpimbor1lem2  47948  smf2id  47950  smfco  47951  smfpimcclem  47956  goldrarr  48067  lambert0  48076  tannpoly  48079  sprsymrelfolem1  48713  sprbisymrel  48720  fmtno0prm  48782  fmtno1prm  48783  fmtno2prm  48784  fmtno3prm  48786  fmtno4prm  48799  m2prm  48815  m3prm  48816  m5prm  48822  m7prm  48824  lighneallem4a  48832  nprmdvdsfacm1lem4  48847  0evenALTV  48925  1oddALTV  48927  2evenALTV  48929  6even  48948  7odd  48949  8even  48950  9gbo  49011  opstrgric  49163  ushggricedg  49164  grtri  49177  usgrexmpl1  49259  usgrexmpl1vtx  49260  usgrexmpl1edg  49261  usgrexmpl2  49264  usgrexmpl2vtx  49265  usgrexmpl2edg  49266  gpgprismgr4cycllem5  49336  pgnbgreunbgr  49362  pgn4cyclex  49363  uspgrex  49387  lmod1zrnlvec  49745  zlmodzxzldeplem1  49751  zlmodzxzldeplem3  49753  zlmodzxzldeplem4  49754  zlmodzxzldep  49755  ldepsnlinclem1  49756  ldepsnlinclem2  49757  blennn0elnn  49828  nn0sumshdiglemA  49870  nn0sumshdiglemB  49871  itcovalpclem2  49922  itcovalt2lem2  49927  ackval42  49947  rrx2line  49991  spheres  49997  2sphere  50000  resipos  50228  functhinclem1  50718  prsthinc  50738  setc1oterm  50765  funcsetc1ocl  50770  funcsetc1o  50771  isinito2lem  50772  isinito3  50774  functermc2  50783  incat  50878  setc1onsubc  50879  parcatid2  50902  parcatid  50903  parmapfunc2  50913  par2diag  50919  fuconuniqlem  50920  fuconuniqvalslem  50922