Theorem eqeltri 2835

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

Syntax hints:   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  eqeltrri  2836  3eltr4i  2852  intab  4908  axrep6g  5212  unisn2  5234  inex2  5246  vpwex  5306  ord3ex  5316  zfpair  5350  vsnex  5364  snex  5368  opex  5403  opexOLD  5404  otex  5405  uniopel  5457  elvvuni  5695  isarep2  6575  fvex  6840  fvexi  6841  riotaex  7317  ovexi  7390  tpex  7689  oprabex  7918  oprabrexex2  7920  mpoexw  8020  mptmpoopabbrd  8022  tfrlem16  8322  1oex  8405  2oex  8406  1on  8407  2on  8408  3on  8411  4on  8412  oesuclem  8450  oecl  8462  o2p2e4  8466  nnecl  8539  1onnALT  8567  2onnALT  8569  3onn  8570  4onn  8571  mapsnf1o2  8832  sbthlem10  9024  cnvfi  9100  fnfi  9102  nnunifi  9191  imafiOLD  9216  pwfi  9219  prfiALT  9225  tpfi  9226  fczfsuppd  9289  cantnfvalf  9577  oemapwe  9606  cantnffval2  9607  cnfcom3clem  9617  ssttrcl  9627  r1fin  9688  hta  9812  infxpenlem  9926  alephon  9982  alephfplem1  10017  dfac5lem4  10039  dfac5lem5  10040  dfac5lem4OLD  10041  kmlem10  10073  fin1a2lem10  10322  fin1a2lem12  10324  hsmexlem9  10338  axcc2lem  10349  domtriomlem  10355  axdc2lem  10361  axcclem  10370  brdom7disj  10444  brdom6disj  10445  iundom2g  10453  konigthlem  10482  canthwelem  10564  wunex2  10652  wunex3  10655  1nq  10842  1pr  10929  nrex1  10978  axcnex  11061  ax1cn  11063  pnfex  11189  mnfxr  11193  cju  12146  nnexALT  12167  2nn  12245  2re  12246  2cn  12247  3nn  12251  3re  12252  3cn  12253  4nn  12255  4re  12256  4cn  12257  5nn  12258  5re  12259  5cn  12260  6nn  12261  6re  12262  6cn  12263  7nn  12264  7re  12265  7cn  12266  8nn  12267  8re  12268  8cn  12269  9nn  12270  9re  12271  9cn  12272  nn0ex  12434  zexALT  12535  nneo  12604  zeo  12606  deccl  12650  10re  12654  decnncl  12655  numnncl2  12658  decnncl2  12659  numsucc  12675  numma2c  12681  numadd  12682  numaddc  12683  nummul1c  12684  nummul2c  12685  decmul1  12699  qexALT  12905  xrex  12928  xnegex  13151  xnegcl  13156  ixxssxr  13301  fz0to4untppr  13575  fz0to5un2tp  13576  om2uzuzi  13902  ltweuz  13914  axdc4uzlem  13936  seqex  13956  seqexw  13970  m1expcl2  14038  faccl  14236  facwordi  14242  faclbnd2  14244  bccl  14275  hashen1  14323  hashrabrsn  14325  hashunlei  14378  hashpw  14389  tpf1o  14454  s1cli  14559  ccat2s1p1  14583  cats1un  14674  revs1  14718  cshwsexa  14777  cats1cli  14810  cats1fvn  14811  crre  15067  remim  15070  climmpt  15524  sumex  15641  supcvg  15812  geo2lim  15831  prodex  15861  bpoly4  16015  ere  16045  eftlub  16067  efsep  16068  tan0  16109  ef01bndlem  16142  nn0o  16343  divalglem5  16357  divalglem9  16361  sadcf  16413  smupf  16438  crth  16739  phimullem  16740  pczpre  16809  pockthi  16869  prmreclem2  16879  igz  16896  0ramcl  16985  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  strle1  17119  ndxarg  17157  basendxnn  17180  plusgndxnn  17239  tsetndxnn  17308  plendxnn  17322  dsndxnn  17341  unifndxnn  17351  prdsbasex  17404  prdsds  17418  yonedalem3  18237  isposix  18281  chnub  18579  plusffval  18605  issubmgm2  18662  efmnd1hash  18851  efmnd2hash  18853  smndex1bas  18868  smndex1sgrp  18870  smndex1mnd  18872  smndex1id  18873  smndex2dbas  18876  smndex2hbas  18878  grpsubfval  18950  mulgfval  19036  symg1hash  19356  symg2hash  19358  symgvalstruct  19363  symgfisg  19434  psgnsn  19486  psgnprfval1  19488  odfval  19498  sylow2alem2  19584  efgsval2  19699  efgsp1  19703  pgpfaclem1  20049  dvdsrval  20332  isirred  20390  scaffval  20870  cnfldex  21350  xrsex  21364  pzriprnglem4  21459  pzriprnglem5  21460  pzriprnglem6  21461  pzriprng1ALT  21471  znle  21511  znidomb  21536  cnmsgnsubg  21552  refld  21594  ipffval  21623  psrbag0  22038  psrbagsn  22039  psr1baslem  22170  mat1dimbas  22455  mat1dimscm  22458  mat1f1o  22461  mat1rhmelval  22463  m2detleib  22614  pmatcoe1fsupp  22684  indistopon  22984  iccordt  23197  conncompid  23414  ptbasfi  23564  ptcmpfi  23796  ustfn  24185  ust0  24203  ustn0  24204  tmslem  24465  nmfval  24571  cnbl0  24756  cnopn  24769  remet  24773  re2ndc  24784  zcld  24797  icccmp  24809  xrge0gsumle  24817  xrge0tsms  24818  xmetdcn  24822  divcn  24853  expcn  24857  iiconn  24872  idcncf  24903  cnmpopc  24913  cnrehmeo  24938  cnheiborlem  24939  rellycmp  24942  bndth  24943  evth2  24945  cnrlmod  25128  cnrlvec  25129  cncmet  25307  ishl2  25355  ehleudis  25403  ehleudisval  25404  finiunmbl  25529  ioombl1lem4  25546  vitalilem4  25596  vitalilem5  25597  ismbf2d  25625  mbfimaopnlem  25640  mbfi1fseqlem6  25705  itgex  25755  bddmulibl  25824  ditgex  25837  recnperf  25890  dvcnvrelem2  26003  ftc1  26027  mdegcl  26052  plyeq0lem  26193  aaliou3lem4  26330  dvradcnv  26404  sincn  26427  coscn  26428  tanabsge  26488  circsubm  26535  reloggim  26581  logcn  26629  dvloglem  26630  logdmopn  26631  dvlog2  26635  2irrexpq  26713  cxpcn  26727  cxpcn3  26730  resqrtcn  26731  2logb9irrALT  26780  2irrexpqALT  26782  atanrecl  26893  atan1  26910  atansopn  26914  birthdaylem1  26933  birthday  26936  emcllem4  26980  emcllem6  26982  lgamgulmlem6  27015  basellem6  27067  ppiublem1  27183  bposlem6  27270  bposlem8  27272  lgslem4  27281  lgsdir2lem2  27307  selberglem1  27526  selberglem3  27528  selberg  27529  selbergs  27555  qdrng  27601  0no  27819  1no  27820  lrrecse  27952  precsexlem11  28227  seqsex  28295  nnsex  28328  n0bday  28362  n0subs  28373  n0p1nns  28381  dfnns2  28382  zsex  28390  bdayfinbndlem1  28477  z12sex  28484  z12shalf  28490  edgfndxnn  29079  structvtxvallem  29107  usgrexmpllem  29347  usgrexmpl  29350  uhgrspan1  29390  upgrres  29393  umgrres  29394  usgrres  29395  upgrres1  29400  umgrres1  29401  usgrres1  29402  fusgrfis  29417  cusgrres  29535  vtxdlfgrval  29572  vtxdusgr0edgnelALT  29583  umgr2v2e  29612  vtxdginducedm1lem1  29626  vtxdginducedm1fi  29631  finsumvtxdg2ssteplem4  29635  pthdlem1  29852  crctcshlem3  29905  2wlkd  30022  2wlkond  30023  2trlond  30025  2pthd  30026  2pthond  30028  umgr2adedgwlkonALT  30033  0pth  30213  wlk2v2e  30245  3wlkd  30258  3trlond  30261  3pthd  30262  3pthond  30263  3spthond  30265  eupthvdres  30323  eulerpathpr  30328  konigsbergumgr  30339  konigsberglem5  30344  konigsberg  30345  ex-lcm  30546  isvciOLD  30669  isnvi  30702  blocni  30894  hmoval  30899  cncph  30908  ipasslem7  30925  siilem2  30941  normlem2  31200  normlem3  31201  normlem6  31204  h0elch  31344  hhssabloilem  31350  hhsssh  31358  spansnji  31735  nonbooli  31740  3oalem5  31755  3oalem6  31756  3oai  31757  mayetes3i  31818  nmcexi  32115  nmbdfnlb  32139  rnelshi  32148  cnlnadjlem5  32160  pjbdlni  32238  golem2  32361  goeqi  32362  dp2clq  32959  rpdp2cl  32960  rpdp2cl2  32961  dpmul100  32975  rpdpcl  32981  xrge0tsmsd  33154  pmtrto1cl  33180  psgnfzto1stlem  33181  fzto1st  33184  psgnfzto1st  33186  nn0omnd  33427  xrge0slmod  33431  qusima  33491  prmidl0  33533  fply1  33641  extvfvcl  33720  ply1degltdimlem  33806  ccfldextdgrr  33856  algextdeglem8  33908  constrfin  33930  2sqr3minply  33964  2sqr3nconstr  33965  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  cos9thpinconstrlem2  33974  circtopn  34021  circcn  34022  zarcmplem  34065  tpr2tp  34088  tpr2rico  34096  ordtprsval  34102  ordtprsuni  34103  ordtrestNEW  34105  ordtrest2NEWlem  34106  ordtrest2NEW  34107  ordtconnlem1  34108  mndpluscn  34110  xrge0pluscn  34124  xrge0mulc1cn  34125  xrge0haus  34128  lmlimxrge0  34132  lmxrge0  34136  qqhcn  34175  qqhucn  34176  esumex  34213  esumcst  34247  hasheuni  34269  esumcvg  34270  prsiga  34315  brsiga  34367  mbfmcnt  34452  sxbrsigalem3  34456  dya2iocuni  34467  dya2iocucvr  34468  sxbrsigalem1  34469  sxbrsiga  34474  eulerpartlemt  34555  fibp1  34585  coinflipprob  34664  coinfliprv  34667  ccatmulgnn0dir  34726  signswplusg  34739  hgt750lem2  34836  hgt750leme  34842  bnj105  34907  bnj918  34949  bnj95  35046  bnj852  35103  bnj865  35105  fineqvnttrclse  35305  subfacp1lem1  35407  subfacp1lem3  35410  subfacp1lem5  35412  subfacp1lem6  35413  kur14lem7  35440  iisconn  35480  iillysconn  35481  cvmliftlem5  35517  cvmliftlem8  35520  cvmliftlem10  35522  cvmlift2lem9  35539  satfv0  35586  goalrlem  35624  goalr  35625  satffunlem2lem2  35634  circum  35902  iexpire  35963  altopex  36188  colinearex  36288  ssoninhaus  36676  cnndvlem2  36844  bj-prex  37393  bj-prfromadj  37398  bj-pinftyccb  37581  taupi  37683  isbasisrelowl  37720  relowlpssretop  37726  poimirlem29  38016  poimirlem30  38017  poimirlem31  38018  dvasin  38071  dvacos  38072  areacirc  38080  upixp  38096  fdc  38112  lmclim2  38125  cncfres  38132  heibor1lem  38176  rrnval  38194  rrnmet  38196  reheibor  38206  isdrngo2  38325  isrngohom  38332  idlval  38380  isidl  38381  igenval  38428  scottexf  38535  cnvepresex  38703  preex  38859  renegclALT  39455  ldualfvadd  39620  cmtfvalN  39702  cvrfval  39760  cdleme31fv  40882  cdlemk40  41409  cdlemk56  41463  dibopelvalN  41635  dibopelval2  41637  dibelval3  41639  diblsmopel  41663  cdlemn11a  41699  dihopelvalcpre  41740  dihpN  41828  hlhilsca  42427  hlhilip  42440  3factsumint1  42506  lcmineqlem23  42536  aks4d1p1p6  42558  aks4d1p1p5  42560  aks6d1c6isolem2  42660  itrere  42795  acos1half  42835  redvmptabs  42837  readvrec2  42838  sn-0tie0  42941  sn-itrere  42978  sn-retire  42979  prjspval  43053  flt4lem5e  43106  sn-isghm  43123  mapfzcons2  43168  jm2.23  43441  jm2.27dlem2  43455  jm2.27dlem4  43457  rmydioph  43459  rmxdioph  43461  expdiophlem2  43467  expdioph  43468  aomclem6  43504  pwslnmlem0  43536  frlmpwfi  43543  mncn0  43584  aaitgo  43607  arearect  43660  areaquad  43661  omcl3g  43779  comptiunov2i  44150  frege110  44417  frege133  44440  scottex2  44689  radcnvrat  44758  uzmptshftfval  44790  dvradcnv2  44791  binomcxplemdvbinom  44797  binomcxplemcvg  44798  binomcxplemnotnn0  44800  permaxinf2lem  45456  rfcnpre1  45467  fcnre  45473  refsumcn  45478  refsum2cnlem1  45485  unirnmapsn  45659  infxrpnf  45889  iocopn  45965  icoopn  45970  mccl  46043  clim1fr1  46046  islptre  46064  sumnnodd  46075  lptre2pt  46083  limclner  46094  limclr  46098  expfac  46100  0cnf  46320  icccncfext  46330  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  itgsin0pilem1  46393  iblempty  46408  itgvol0  46411  stoweidlem47  46490  stoweidlem53  46496  stoweidlem57  46500  stoweidlem59  46502  wallispilem3  46510  wallispilem4  46511  wallispilem5  46512  wallispi  46513  stirlinglem1  46517  stirlinglem8  46524  stirlinglem12  46528  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  dirkerper  46539  dirkercncflem2  46547  fourierdlem16  46566  fourierdlem21  46571  fourierdlem22  46572  fourierdlem36  46586  fourierdlem42  46592  fourierdlem71  46620  fourierdlem83  46632  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  fourierdlem114  46663  sqwvfoura  46671  sqwvfourb  46672  fourierswlem  46673  fouriersw  46674  etransclem48  46725  salexct3  46785  salgencntex  46786  salgensscntex  46787  iooborel  46794  bor1sal  46798  gsumge0cl  46814  sge0tsms  46823  sge0isum  46870  nnfoctbdjlem  46898  isomenndlem  46973  mbfresmf  47182  incsmflem  47184  incsmf  47185  smfmbfcex  47203  decsmflem  47209  decsmf  47210  smflimlem1  47214  smfpimbor1lem2  47242  smf2id  47244  smfco  47245  smfpimcclem  47250  goldrarr  47344  lambert0  47350  sprsymrelfolem1  47967  sprbisymrel  47974  fmtno0prm  48036  fmtno1prm  48037  fmtno2prm  48038  fmtno3prm  48040  fmtno4prm  48053  m2prm  48069  m3prm  48070  m5prm  48076  m7prm  48078  lighneallem4a  48086  nprmdvdsfacm1lem4  48101  0evenALTV  48179  1oddALTV  48181  2evenALTV  48183  6even  48202  7odd  48203  8even  48204  9gbo  48265  opstrgric  48417  ushggricedg  48418  grtri  48431  usgrexmpl1  48513  usgrexmpl1vtx  48514  usgrexmpl1edg  48515  usgrexmpl2  48518  usgrexmpl2vtx  48519  usgrexmpl2edg  48520  gpgprismgr4cycllem5  48590  pgnbgreunbgr  48616  pgn4cyclex  48617  uspgrex  48641  lmod1zrnlvec  48985  zlmodzxzldeplem1  48991  zlmodzxzldeplem3  48993  zlmodzxzldeplem4  48994  zlmodzxzldep  48995  ldepsnlinclem1  48996  ldepsnlinclem2  48997  blennn0elnn  49068  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  itcovalpclem2  49162  itcovalt2lem2  49167  ackval42  49187  rrx2line  49231  rrx2linesl  49234  spheres  49237  2sphere  49240  2sphere0  49241  line2x  49245  line2y  49246  resipos  49465  functhinclem1  49934  prsthinc  49954  setc1oterm  49981  funcsetc1ocl  49986  funcsetc1o  49987  isinito2lem  49988  isinito3  49990  functermc2  49999  incat  50091  setc1onsubc  50092