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 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

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

This theorem is referenced by:  eqeltrri  2831  3eltr4i  2847  intab  4931  axrep6g  5233  unisn2  5255  inex2  5261  vpwex  5320  ord3ex  5330  zfpair  5364  vsnex  5377  opex  5410  otex  5411  uniopel  5462  elvvuni  5699  isarep2  6580  fvex  6845  fvexi  6846  riotaex  7317  ovexi  7390  tpex  7689  oprabex  7918  oprabrexex2  7920  mpoexw  8020  mptmpoopabbrd  8022  mptmpoopabbrdOLD  8023  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  8830  sbthlem10  9022  cnvfi  9098  fnfi  9100  nnunifi  9189  imafiOLD  9214  pwfi  9217  prfiALT  9223  tpfi  9224  fczfsuppd  9287  cantnfvalf  9572  oemapwe  9601  cantnffval2  9602  cnfcom3clem  9612  ssttrcl  9622  r1fin  9683  hta  9807  infxpenlem  9921  alephon  9977  alephfplem1  10012  dfac5lem4  10034  dfac5lem5  10035  dfac5lem4OLD  10036  kmlem10  10068  fin1a2lem10  10317  fin1a2lem12  10319  hsmexlem9  10333  axcc2lem  10344  domtriomlem  10350  axdc2lem  10356  axcclem  10365  brdom7disj  10439  brdom6disj  10440  iundom2g  10448  konigthlem  10477  canthwelem  10559  wunex2  10647  wunex3  10650  1nq  10837  1pr  10924  nrex1  10973  axcnex  11056  ax1cn  11058  pnfex  11183  mnfxr  11187  cju  12139  nnexALT  12145  2nn  12216  2re  12217  2cn  12218  3nn  12222  3re  12223  3cn  12224  4nn  12226  4re  12227  4cn  12228  5nn  12229  5re  12230  5cn  12231  6nn  12232  6re  12233  6cn  12234  7nn  12235  7re  12236  7cn  12237  8nn  12238  8re  12239  8cn  12240  9nn  12241  9re  12242  9cn  12243  nn0ex  12405  zexALT  12506  nneo  12574  zeo  12576  deccl  12620  10re  12624  decnncl  12625  numnncl2  12628  decnncl2  12629  numsucc  12645  numma2c  12651  numadd  12652  numaddc  12653  nummul1c  12654  nummul2c  12655  decmul1  12669  qexALT  12875  xrex  12898  xnegex  13121  xnegcl  13126  ixxssxr  13271  fz0to4untppr  13544  fz0to5un2tp  13545  om2uzuzi  13870  ltweuz  13882  axdc4uzlem  13904  seqex  13924  seqexw  13938  m1expcl2  14006  faccl  14204  facwordi  14210  faclbnd2  14212  bccl  14243  hashen1  14291  hashrabrsn  14293  hashunlei  14346  hashpw  14357  tpf1o  14422  s1cli  14527  ccat2s1p1  14551  cats1un  14642  revs1  14686  cshwsexa  14745  cats1cli  14778  cats1fvn  14779  crre  15035  remim  15038  climmpt  15492  sumex  15609  supcvg  15777  geo2lim  15796  prodex  15826  bpoly4  15980  ere  16010  eftlub  16032  efsep  16033  tan0  16074  ef01bndlem  16107  nn0o  16308  divalglem5  16322  divalglem9  16326  sadcf  16378  smupf  16403  crth  16703  phimullem  16704  pczpre  16773  pockthi  16833  prmreclem2  16843  igz  16860  0ramcl  16949  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  1259prm  17061  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001lem4  17069  4001prm  17070  strle1  17083  ndxarg  17121  basendxnn  17144  plusgndxnn  17203  tsetndxnn  17272  plendxnn  17286  dsndxnn  17305  unifndxnn  17315  prdsbasex  17368  prdsds  17382  yonedalem3  18201  isposix  18245  chnub  18543  plusffval  18569  issubmgm2  18626  efmnd1hash  18815  efmnd2hash  18817  smndex1bas  18829  smndex1sgrp  18831  smndex1mnd  18833  smndex1id  18834  smndex2dbas  18837  smndex2hbas  18839  grpsubfval  18911  mulgfval  18997  symg1hash  19317  symg2hash  19319  symgvalstruct  19324  symgfisg  19395  psgnsn  19447  psgnprfval1  19449  odfval  19459  sylow2alem2  19545  efgsval2  19660  efgsp1  19664  pgpfaclem1  20010  dvdsrval  20295  isirred  20353  scaffval  20829  cnfldex  21310  xrsex  21337  pzriprnglem4  21437  pzriprnglem5  21438  pzriprnglem6  21439  pzriprng1ALT  21449  znle  21489  znidomb  21514  cnmsgnsubg  21530  refld  21572  ipffval  21601  psrbag0  22015  psrbagsn  22016  psr1baslem  22123  mat1dimbas  22414  mat1dimscm  22417  mat1f1o  22420  mat1rhmelval  22422  m2detleib  22573  pmatcoe1fsupp  22643  indistopon  22943  iccordt  23156  conncompid  23373  ptbasfi  23523  ptcmpfi  23755  ustfn  24144  ust0  24162  ustn0  24163  tmslem  24424  nmfval  24530  cnbl0  24715  cnopn  24728  remet  24732  re2ndc  24743  zcld  24756  icccmp  24768  xrge0gsumle  24776  xrge0tsms  24777  xmetdcn  24781  divcnOLD  24811  divcn  24813  expcn  24817  expcnOLD  24819  iiconn  24834  idcncf  24865  cnmpopc  24876  cnrehmeo  24905  cnrehmeoOLD  24906  cnheiborlem  24907  rellycmp  24910  bndth  24911  evth2  24913  cnrlmod  25097  cnrlvec  25098  cncmet  25276  ishl2  25324  ehleudis  25372  ehleudisval  25373  finiunmbl  25499  ioombl1lem4  25516  vitalilem4  25566  vitalilem5  25567  ismbf2d  25595  mbfimaopnlem  25610  mbfi1fseqlem6  25675  itgex  25725  bddmulibl  25794  ditgex  25807  recnperf  25860  dvcnvrelem2  25977  ftc1  26003  mdegcl  26028  plyeq0lem  26169  aaliou3lem4  26308  dvradcnv  26384  sincn  26408  coscn  26409  tanabsge  26469  circsubm  26516  reloggim  26562  logcn  26610  dvloglem  26611  logdmopn  26612  dvlog2  26616  2irrexpq  26694  cxpcn  26708  cxpcnOLD  26709  cxpcn3  26712  resqrtcn  26713  2logb9irrALT  26762  2irrexpqALT  26764  atanrecl  26875  atan1  26892  atansopn  26896  birthdaylem1  26915  birthday  26918  emcllem4  26963  emcllem6  26965  lgamgulmlem6  26998  basellem6  27050  ppiublem1  27167  bposlem6  27254  bposlem8  27256  lgslem4  27265  lgsdir2lem2  27291  selberglem1  27510  selberglem3  27512  selberg  27513  selbergs  27539  qdrng  27585  0sno  27797  1sno  27798  lrrecse  27912  precsexlem11  28185  seqsex  28246  nnsex  28279  n0sbday  28312  n0subs  28322  n0p1nns  28329  dfnns2  28330  zsex  28338  zs12ex  28423  zs12half  28429  edgfndxnn  29014  structvtxvallem  29042  usgrexmpllem  29282  usgrexmpl  29285  uhgrspan1  29325  upgrres  29328  umgrres  29329  usgrres  29330  upgrres1  29335  umgrres1  29336  usgrres1  29337  fusgrfis  29352  cusgrres  29471  vtxdlfgrval  29508  vtxdusgr0edgnelALT  29519  umgr2v2e  29548  vtxdginducedm1lem1  29562  vtxdginducedm1fi  29567  finsumvtxdg2ssteplem4  29571  pthdlem1  29788  crctcshlem3  29841  2wlkd  29958  2wlkond  29959  2trlond  29961  2pthd  29962  2pthond  29964  umgr2adedgwlkonALT  29969  0pth  30149  wlk2v2e  30181  3wlkd  30194  3trlond  30197  3pthd  30198  3pthond  30199  3spthond  30201  eupthvdres  30259  eulerpathpr  30264  konigsbergumgr  30275  konigsberglem5  30280  konigsberg  30281  ex-lcm  30482  isvciOLD  30604  isnvi  30637  blocni  30829  hmoval  30834  cncph  30843  ipasslem7  30860  siilem2  30876  normlem2  31135  normlem3  31136  normlem6  31139  h0elch  31279  hhssabloilem  31285  hhsssh  31293  spansnji  31670  nonbooli  31675  3oalem5  31690  3oalem6  31691  3oai  31692  mayetes3i  31753  nmcexi  32050  nmbdfnlb  32074  rnelshi  32083  cnlnadjlem5  32095  pjbdlni  32173  golem2  32296  goeqi  32297  dp2clq  32911  rpdp2cl  32912  rpdp2cl2  32913  dpmul100  32927  rpdpcl  32933  xrge0tsmsd  33104  pmtrto1cl  33130  psgnfzto1stlem  33131  fzto1st  33134  psgnfzto1st  33136  nn0omnd  33374  xrge0slmod  33378  qusima  33438  prmidl0  33480  fply1  33588  extvfvcl  33650  ply1degltdimlem  33728  ccfldextdgrr  33778  algextdeglem8  33830  constrfin  33852  2sqr3minply  33886  2sqr3nconstr  33887  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  cos9thpinconstrlem2  33896  circtopn  33943  circcn  33944  zarcmplem  33987  tpr2tp  34010  tpr2rico  34018  ordtprsval  34024  ordtprsuni  34025  ordtrestNEW  34027  ordtrest2NEWlem  34028  ordtrest2NEW  34029  ordtconnlem1  34030  mndpluscn  34032  xrge0pluscn  34046  xrge0mulc1cn  34047  xrge0haus  34050  lmlimxrge0  34054  lmxrge0  34058  qqhcn  34097  qqhucn  34098  esumex  34135  esumcst  34169  hasheuni  34191  esumcvg  34192  prsiga  34237  brsiga  34289  mbfmcnt  34374  sxbrsigalem3  34378  dya2iocuni  34389  dya2iocucvr  34390  sxbrsigalem1  34391  sxbrsiga  34396  eulerpartlemt  34477  fibp1  34507  coinflipprob  34586  coinfliprv  34589  ccatmulgnn0dir  34648  signswplusg  34661  hgt750lem2  34758  hgt750leme  34764  bnj105  34829  bnj918  34871  bnj95  34969  bnj852  35026  bnj865  35028  fineqvnttrclse  35229  subfacp1lem1  35322  subfacp1lem3  35325  subfacp1lem5  35327  subfacp1lem6  35328  kur14lem7  35355  iisconn  35395  iillysconn  35396  cvmliftlem5  35432  cvmliftlem8  35435  cvmliftlem10  35437  cvmlift2lem9  35454  satfv0  35501  goalrlem  35539  goalr  35540  satffunlem2lem2  35549  circum  35817  iexpire  35878  altopex  36103  colinearex  36203  ssoninhaus  36591  cnndvlem2  36681  bj-prex  37184  bj-prfromadj  37189  bj-pinftyccb  37365  taupi  37467  isbasisrelowl  37502  relowlpssretop  37508  poimirlem29  37789  poimirlem30  37790  poimirlem31  37791  dvasin  37844  dvacos  37845  areacirc  37853  upixp  37869  fdc  37885  lmclim2  37898  cncfres  37905  heibor1lem  37949  rrnval  37967  rrnmet  37969  reheibor  37979  isdrngo2  38098  isrngohom  38105  idlval  38153  isidl  38154  igenval  38201  scottexf  38308  cnvepresex  38468  preex  38604  renegclALT  39162  ldualfvadd  39327  cmtfvalN  39409  cvrfval  39467  cdleme31fv  40589  cdlemk40  41116  cdlemk56  41170  dibopelvalN  41342  dibopelval2  41344  dibelval3  41346  diblsmopel  41370  cdlemn11a  41406  dihopelvalcpre  41447  dihpN  41535  hlhilsca  42134  hlhilip  42147  3factsumint1  42214  lcmineqlem23  42244  aks4d1p1p6  42266  aks4d1p1p5  42268  aks6d1c6isolem2  42368  itrere  42515  acos1half  42555  redvmptabs  42557  readvrec2  42558  sn-0tie0  42648  sn-itrere  42685  sn-retire  42686  prjspval  42788  flt4lem5e  42841  sn-isghm  42858  mapfzcons2  42903  jm2.23  43180  jm2.27dlem2  43194  jm2.27dlem4  43196  rmydioph  43198  rmxdioph  43200  expdiophlem2  43206  expdioph  43207  aomclem6  43243  pwslnmlem0  43275  frlmpwfi  43282  mncn0  43323  aaitgo  43346  arearect  43399  areaquad  43400  omcl3g  43518  comptiunov2i  43889  frege110  44156  frege133  44179  scottex2  44428  radcnvrat  44497  uzmptshftfval  44529  dvradcnv2  44530  binomcxplemdvbinom  44536  binomcxplemcvg  44537  binomcxplemnotnn0  44539  permaxinf2lem  45195  rfcnpre1  45206  fcnre  45212  refsumcn  45217  refsum2cnlem1  45224  unirnmapsn  45400  infxrpnf  45632  iocopn  45708  icoopn  45713  mccl  45786  clim1fr1  45789  islptre  45807  sumnnodd  45818  lptre2pt  45826  limclner  45837  limclr  45841  expfac  45843  0cnf  46063  icccncfext  46073  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  itgsin0pilem1  46136  iblempty  46151  itgvol0  46154  stoweidlem47  46233  stoweidlem53  46239  stoweidlem57  46243  stoweidlem59  46245  wallispilem3  46253  wallispilem4  46254  wallispilem5  46255  wallispi  46256  stirlinglem1  46260  stirlinglem8  46267  stirlinglem12  46271  stirlinglem13  46272  stirlinglem14  46273  stirlinglem15  46274  dirkerper  46282  dirkercncflem2  46290  fourierdlem16  46309  fourierdlem21  46314  fourierdlem22  46315  fourierdlem36  46329  fourierdlem42  46335  fourierdlem71  46363  fourierdlem83  46375  fourierdlem102  46394  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  fourierdlem112  46404  fourierdlem114  46406  sqwvfoura  46414  sqwvfourb  46415  fourierswlem  46416  fouriersw  46417  etransclem48  46468  salexct3  46528  salgencntex  46529  salgensscntex  46530  iooborel  46537  bor1sal  46541  gsumge0cl  46557  sge0tsms  46566  sge0isum  46613  nnfoctbdjlem  46641  isomenndlem  46716  mbfresmf  46925  incsmflem  46927  incsmf  46928  smfmbfcex  46946  decsmflem  46952  decsmf  46953  smflimlem1  46957  smfpimbor1lem2  46985  smf2id  46987  smfco  46988  smfpimcclem  46993  lambert0  47075  sprsymrelfolem1  47680  sprbisymrel  47687  fmtno0prm  47746  fmtno1prm  47747  fmtno2prm  47748  fmtno3prm  47750  fmtno4prm  47763  m2prm  47779  m3prm  47780  m5prm  47786  m7prm  47788  lighneallem4a  47796  0evenALTV  47876  1oddALTV  47878  2evenALTV  47880  6even  47899  7odd  47900  8even  47901  9gbo  47962  opstrgric  48114  ushggricedg  48115  grtri  48128  usgrexmpl1  48210  usgrexmpl1vtx  48211  usgrexmpl1edg  48212  usgrexmpl2  48215  usgrexmpl2vtx  48216  usgrexmpl2edg  48217  gpgprismgr4cycllem5  48287  pgnbgreunbgr  48313  pgn4cyclex  48314  uspgrex  48338  lmod1zrnlvec  48682  zlmodzxzldeplem1  48688  zlmodzxzldeplem3  48690  zlmodzxzldeplem4  48691  zlmodzxzldep  48692  ldepsnlinclem1  48693  ldepsnlinclem2  48694  blennn0elnn  48765  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  itcovalpclem2  48859  itcovalt2lem2  48864  ackval42  48884  rrx2line  48928  rrx2linesl  48931  spheres  48934  2sphere  48937  2sphere0  48938  line2x  48942  line2y  48943  resipos  49162  functhinclem1  49631  prsthinc  49651  setc1oterm  49678  funcsetc1ocl  49683  funcsetc1o  49684  isinito2lem  49685  isinito3  49687  functermc2  49696  incat  49788  setc1onsubc  49789