Theorem eqeltri 2824

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

Syntax hints:   = wceq 1540   ∈ wcel 2109

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqeltrri  2825  3eltr4i  2841  intab  4938  axrep6g  5240  unisn2  5262  inex2  5268  vpwex  5327  ord3ex  5337  zfpair  5371  vsnex  5384  opex  5419  otex  5420  uniopel  5471  elvvuni  5708  isarep2  6590  fvex  6853  fvexi  6854  riotaex  7330  ovexi  7403  tpex  7702  oprabex  7934  oprabrexex2  7936  mpoexw  8036  mptmpoopabbrd  8038  mptmpoopabbrdOLD  8039  tfrlem16  8338  1oex  8421  2oex  8422  1on  8423  2on  8424  3on  8427  4on  8428  oesuclem  8466  oecl  8478  o2p2e4  8482  nnecl  8554  1onnALT  8582  2onnALT  8584  3onn  8585  4onn  8586  mapsnf1o2  8844  sbthlem10  9037  cnvfi  9117  fnfi  9119  nnunifi  9214  imafiOLD  9241  pwfi  9244  xpfiOLD  9246  prfiALT  9251  tpfi  9252  fczfsuppd  9313  cantnfvalf  9594  oemapwe  9623  cantnffval2  9624  cnfcom3clem  9634  ssttrcl  9644  r1fin  9702  hta  9826  infxpenlem  9942  alephon  9998  alephfplem1  10033  dfac5lem4  10055  dfac5lem5  10056  dfac5lem4OLD  10057  kmlem10  10089  fin1a2lem10  10338  fin1a2lem12  10340  hsmexlem9  10354  axcc2lem  10365  domtriomlem  10371  axdc2lem  10377  axcclem  10386  brdom7disj  10460  brdom6disj  10461  iundom2g  10469  konigthlem  10497  canthwelem  10579  wunex2  10667  wunex3  10670  1nq  10857  1pr  10944  nrex1  10993  axcnex  11076  ax1cn  11078  pnfex  11203  mnfxr  11207  cju  12158  nnexALT  12164  2nn  12235  2re  12236  2cn  12237  3nn  12241  3re  12242  3cn  12243  4nn  12245  4re  12246  4cn  12247  5nn  12248  5re  12249  5cn  12250  6nn  12251  6re  12252  6cn  12253  7nn  12254  7re  12255  7cn  12256  8nn  12257  8re  12258  8cn  12259  9nn  12260  9re  12261  9cn  12262  nn0ex  12424  zexALT  12525  nneo  12594  zeo  12596  deccl  12640  10re  12644  decnncl  12645  numnncl2  12648  decnncl2  12649  numsucc  12665  numma2c  12671  numadd  12672  numaddc  12673  nummul1c  12674  nummul2c  12675  decmul1  12689  qexALT  12899  xrex  12922  xnegex  13144  xnegcl  13149  ixxssxr  13294  fz0to4untppr  13567  fz0to5un2tp  13568  om2uzuzi  13890  ltweuz  13902  axdc4uzlem  13924  seqex  13944  seqexw  13958  m1expcl2  14026  faccl  14224  facwordi  14230  faclbnd2  14232  bccl  14263  hashen1  14311  hashrabrsn  14313  hashunlei  14366  hashpw  14377  tpf1o  14442  s1cli  14546  ccat2s1p1  14570  cats1un  14662  revs1  14706  cshwsexa  14765  cshwsexaOLD  14766  cats1cli  14799  cats1fvn  14800  crre  15056  remim  15059  climmpt  15513  sumex  15630  supcvg  15798  geo2lim  15817  prodex  15847  bpoly4  16001  ere  16031  eftlub  16053  efsep  16054  tan0  16095  ef01bndlem  16128  nn0o  16329  divalglem5  16343  divalglem9  16347  sadcf  16399  smupf  16424  crth  16724  phimullem  16725  pczpre  16794  pockthi  16854  prmreclem2  16864  igz  16881  0ramcl  16970  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  strle1  17104  ndxarg  17142  basendxnn  17165  plusgndxnn  17224  tsetndxnn  17293  plendxnn  17307  dsndxnn  17326  unifndxnn  17336  prdsbasex  17389  prdsds  17403  yonedalem3  18217  isposix  18261  plusffval  18549  issubmgm2  18606  efmnd1hash  18795  efmnd2hash  18797  smndex1bas  18809  smndex1sgrp  18811  smndex1mnd  18813  smndex1id  18814  smndex2dbas  18817  smndex2hbas  18819  grpsubfval  18891  mulgfval  18977  symg1hash  19296  symg2hash  19298  symgvalstruct  19303  symgfisg  19374  psgnsn  19426  psgnprfval1  19428  odfval  19438  sylow2alem2  19524  efgsval2  19639  efgsp1  19643  pgpfaclem1  19989  dvdsrval  20246  isirred  20304  scaffval  20762  cnfldex  21243  xrsex  21270  pzriprnglem4  21370  pzriprnglem5  21371  pzriprnglem6  21372  pzriprng1ALT  21382  znle  21422  znidomb  21447  cnmsgnsubg  21462  refld  21504  ipffval  21533  psrbag0  21945  psrbagsn  21946  psr1baslem  22045  mat1dimbas  22335  mat1dimscm  22338  mat1f1o  22341  mat1rhmelval  22343  m2detleib  22494  pmatcoe1fsupp  22564  indistopon  22864  iccordt  23077  conncompid  23294  ptbasfi  23444  ptcmpfi  23676  ustfn  24065  ust0  24083  ustn0  24084  tmslem  24346  nmfval  24452  cnbl0  24637  cnopn  24650  remet  24654  re2ndc  24665  zcld  24678  icccmp  24690  xrge0gsumle  24698  xrge0tsms  24699  xmetdcn  24703  divcnOLD  24733  divcn  24735  expcn  24739  expcnOLD  24741  iiconn  24756  idcncf  24787  cnmpopc  24798  cnrehmeo  24827  cnrehmeoOLD  24828  cnheiborlem  24829  rellycmp  24832  bndth  24833  evth2  24835  cnrlmod  25019  cnrlvec  25020  cncmet  25198  ishl2  25246  ehleudis  25294  ehleudisval  25295  finiunmbl  25421  ioombl1lem4  25438  vitalilem4  25488  vitalilem5  25489  ismbf2d  25517  mbfimaopnlem  25532  mbfi1fseqlem6  25597  itgex  25647  bddmulibl  25716  ditgex  25729  recnperf  25782  dvcnvrelem2  25899  ftc1  25925  mdegcl  25950  plyeq0lem  26091  aaliou3lem4  26230  dvradcnv  26306  sincn  26330  coscn  26331  tanabsge  26391  circsubm  26438  reloggim  26484  logcn  26532  dvloglem  26533  logdmopn  26534  dvlog2  26538  2irrexpq  26616  cxpcn  26630  cxpcnOLD  26631  cxpcn3  26634  resqrtcn  26635  2logb9irrALT  26684  2irrexpqALT  26686  atanrecl  26797  atan1  26814  atansopn  26818  birthdaylem1  26837  birthday  26840  emcllem4  26885  emcllem6  26887  lgamgulmlem6  26920  basellem6  26972  ppiublem1  27089  bposlem6  27176  bposlem8  27178  lgslem4  27187  lgsdir2lem2  27213  selberglem1  27432  selberglem3  27434  selberg  27435  selbergs  27461  qdrng  27507  0sno  27714  1sno  27715  lrrecse  27825  precsexlem11  28095  seqsex  28155  nnsex  28187  n0sbday  28220  n0subs  28229  n0p1nns  28236  dfnns2  28237  zsex  28244  zs12ex  28314  edgfndxnn  28895  structvtxvallem  28923  usgrexmpllem  29163  usgrexmpl  29166  uhgrspan1  29206  upgrres  29209  umgrres  29210  usgrres  29211  upgrres1  29216  umgrres1  29217  usgrres1  29218  fusgrfis  29233  cusgrres  29352  vtxdlfgrval  29389  vtxdusgr0edgnelALT  29400  umgr2v2e  29429  vtxdginducedm1lem1  29443  vtxdginducedm1fi  29448  finsumvtxdg2ssteplem4  29452  pthdlem1  29669  crctcshlem3  29722  2wlkd  29839  2wlkond  29840  2trlond  29842  2pthd  29843  2pthond  29845  umgr2adedgwlkonALT  29850  0pth  30027  wlk2v2e  30059  3wlkd  30072  3trlond  30075  3pthd  30076  3pthond  30077  3spthond  30079  eupthvdres  30137  eulerpathpr  30142  konigsbergumgr  30153  konigsberglem5  30158  konigsberg  30159  ex-lcm  30360  isvciOLD  30482  isnvi  30515  blocni  30707  hmoval  30712  cncph  30721  ipasslem7  30738  siilem2  30754  normlem2  31013  normlem3  31014  normlem6  31017  h0elch  31157  hhssabloilem  31163  hhsssh  31171  spansnji  31548  nonbooli  31553  3oalem5  31568  3oalem6  31569  3oai  31570  mayetes3i  31631  nmcexi  31928  nmbdfnlb  31952  rnelshi  31961  cnlnadjlem5  31973  pjbdlni  32051  golem2  32174  goeqi  32175  dp2clq  32774  rpdp2cl  32775  rpdp2cl2  32776  dpmul100  32790  rpdpcl  32796  chnub  32911  xrge0tsmsd  32975  pmtrto1cl  33029  psgnfzto1stlem  33030  fzto1st  33033  psgnfzto1st  33035  nn0omnd  33289  xrge0slmod  33292  qusima  33352  prmidl0  33394  fply1  33500  ply1degltdimlem  33591  ccfldextdgrr  33640  algextdeglem8  33687  constrfin  33709  2sqr3minply  33743  2sqr3nconstr  33744  cos9thpiminplylem4  33748  cos9thpiminplylem5  33749  cos9thpinconstrlem2  33753  circtopn  33800  circcn  33801  zarcmplem  33844  tpr2tp  33867  tpr2rico  33875  ordtprsval  33881  ordtprsuni  33882  ordtrestNEW  33884  ordtrest2NEWlem  33885  ordtrest2NEW  33886  ordtconnlem1  33887  mndpluscn  33889  xrge0pluscn  33903  xrge0mulc1cn  33904  xrge0haus  33907  lmlimxrge0  33911  lmxrge0  33915  qqhcn  33954  qqhucn  33955  esumex  33992  esumcst  34026  hasheuni  34048  esumcvg  34049  prsiga  34094  brsiga  34146  mbfmcnt  34232  sxbrsigalem3  34236  dya2iocuni  34247  dya2iocucvr  34248  sxbrsigalem1  34249  sxbrsiga  34254  eulerpartlemt  34335  fibp1  34365  coinflipprob  34444  coinfliprv  34447  ccatmulgnn0dir  34506  signswplusg  34519  hgt750lem2  34616  hgt750leme  34622  bnj105  34687  bnj918  34729  bnj95  34827  bnj852  34884  bnj865  34886  subfacp1lem1  35139  subfacp1lem3  35142  subfacp1lem5  35144  subfacp1lem6  35145  kur14lem7  35172  iisconn  35212  iillysconn  35213  cvmliftlem5  35249  cvmliftlem8  35252  cvmliftlem10  35254  cvmlift2lem9  35271  satfv0  35318  goalrlem  35356  goalr  35357  satffunlem2lem2  35366  circum  35634  iexpire  35695  altopex  35921  colinearex  36021  ssoninhaus  36409  cnndvlem2  36499  bj-prex  37001  bj-prfromadj  37006  bj-pinftyccb  37182  taupi  37284  isbasisrelowl  37319  relowlpssretop  37325  poimirlem29  37616  poimirlem30  37617  poimirlem31  37618  dvasin  37671  dvacos  37672  areacirc  37680  upixp  37696  fdc  37712  lmclim2  37725  cncfres  37732  heibor1lem  37776  rrnval  37794  rrnmet  37796  reheibor  37806  isdrngo2  37925  isrngohom  37932  idlval  37980  isidl  37981  igenval  38028  scottexf  38135  cnvepresex  38291  renegclALT  38929  ldualfvadd  39094  cmtfvalN  39176  cvrfval  39234  cdleme31fv  40357  cdlemk40  40884  cdlemk56  40938  dibopelvalN  41110  dibopelval2  41112  dibelval3  41114  diblsmopel  41138  cdlemn11a  41174  dihopelvalcpre  41215  dihpN  41303  hlhilsca  41902  hlhilip  41915  3factsumint1  41982  lcmineqlem23  42012  aks4d1p1p6  42034  aks4d1p1p5  42036  aks6d1c6isolem2  42136  itrere  42279  acos1half  42319  redvmptabs  42321  readvrec2  42322  sn-0tie0  42412  sn-itrere  42449  sn-retire  42450  prjspval  42564  flt4lem5e  42617  sn-isghm  42634  mapfzcons2  42680  jm2.23  42958  jm2.27dlem2  42972  jm2.27dlem4  42974  rmydioph  42976  rmxdioph  42978  expdiophlem2  42984  expdioph  42985  aomclem6  43021  pwslnmlem0  43053  frlmpwfi  43060  mncn0  43101  aaitgo  43124  arearect  43177  areaquad  43178  omcl3g  43296  comptiunov2i  43668  frege110  43935  frege133  43958  scottex2  44207  radcnvrat  44276  uzmptshftfval  44308  dvradcnv2  44309  binomcxplemdvbinom  44315  binomcxplemcvg  44316  binomcxplemnotnn0  44318  permaxinf2lem  44975  rfcnpre1  44986  fcnre  44992  refsumcn  44997  refsum2cnlem1  45004  unirnmapsn  45181  infxrpnf  45415  iocopn  45491  icoopn  45496  mccl  45569  clim1fr1  45572  islptre  45590  sumnnodd  45601  lptre2pt  45611  limclner  45622  limclr  45626  expfac  45628  0cnf  45848  icccncfext  45858  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  itgsin0pilem1  45921  iblempty  45936  itgvol0  45939  stoweidlem47  46018  stoweidlem53  46024  stoweidlem57  46028  stoweidlem59  46030  wallispilem3  46038  wallispilem4  46039  wallispilem5  46040  wallispi  46041  stirlinglem1  46045  stirlinglem8  46052  stirlinglem12  46056  stirlinglem13  46057  stirlinglem14  46058  stirlinglem15  46059  dirkerper  46067  dirkercncflem2  46075  fourierdlem16  46094  fourierdlem21  46099  fourierdlem22  46100  fourierdlem36  46114  fourierdlem42  46120  fourierdlem71  46148  fourierdlem83  46160  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fourierdlem112  46189  fourierdlem114  46191  sqwvfoura  46199  sqwvfourb  46200  fourierswlem  46201  fouriersw  46202  etransclem48  46253  salexct3  46313  salgencntex  46314  salgensscntex  46315  iooborel  46322  bor1sal  46326  gsumge0cl  46342  sge0tsms  46351  sge0isum  46398  nnfoctbdjlem  46426  isomenndlem  46501  mbfresmf  46710  incsmflem  46712  incsmf  46713  smfmbfcex  46731  decsmflem  46737  decsmf  46738  smflimlem1  46742  smfpimbor1lem2  46770  smf2id  46772  smfco  46773  smfpimcclem  46778  tworepnotupword  46857  lambert0  46861  sprsymrelfolem1  47466  sprbisymrel  47473  fmtno0prm  47532  fmtno1prm  47533  fmtno2prm  47534  fmtno3prm  47536  fmtno4prm  47549  m2prm  47565  m3prm  47566  m5prm  47572  m7prm  47574  lighneallem4a  47582  0evenALTV  47662  1oddALTV  47664  2evenALTV  47666  6even  47685  7odd  47686  8even  47687  9gbo  47748  opstrgric  47899  ushggricedg  47900  grtri  47912  usgrexmpl1  47986  usgrexmpl1vtx  47987  usgrexmpl1edg  47988  usgrexmpl2  47991  usgrexmpl2vtx  47992  usgrexmpl2edg  47993  gpgprismgr4cycllem5  48062  pgnbgreunbgr  48088  pgn4cyclex  48089  uspgrex  48111  lmod1zrnlvec  48456  zlmodzxzldeplem1  48462  zlmodzxzldeplem3  48464  zlmodzxzldeplem4  48465  zlmodzxzldep  48466  ldepsnlinclem1  48467  ldepsnlinclem2  48468  blennn0elnn  48539  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  itcovalpclem2  48633  itcovalt2lem2  48638  ackval42  48658  rrx2line  48702  rrx2linesl  48705  spheres  48708  2sphere  48711  2sphere0  48712  line2x  48716  line2y  48717  resipos  48936  functhinclem1  49406  prsthinc  49426  setc1oterm  49453  funcsetc1ocl  49458  funcsetc1o  49459  isinito2lem  49460  isinito3  49462  functermc2  49471  incat  49563  setc1onsubc  49564