Theorem eqeltri 2833

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

Syntax hints:   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eqeltrri  2834  3eltr4i  2850  intab  4935  axrep6g  5237  unisn2  5259  inex2  5265  vpwex  5324  ord3ex  5334  zfpair  5368  vsnex  5381  snex  5385  opex  5419  opexOLD  5420  otex  5421  uniopel  5472  elvvuni  5709  isarep2  6590  fvex  6855  fvexi  6856  riotaex  7329  ovexi  7402  tpex  7701  oprabex  7930  oprabrexex2  7932  mpoexw  8032  mptmpoopabbrd  8034  mptmpoopabbrdOLD  8035  tfrlem16  8334  1oex  8417  2oex  8418  1on  8419  2on  8420  3on  8423  4on  8424  oesuclem  8462  oecl  8474  o2p2e4  8478  nnecl  8551  1onnALT  8579  2onnALT  8581  3onn  8582  4onn  8583  mapsnf1o2  8844  sbthlem10  9036  cnvfi  9112  fnfi  9114  nnunifi  9203  imafiOLD  9228  pwfi  9231  prfiALT  9237  tpfi  9238  fczfsuppd  9301  cantnfvalf  9586  oemapwe  9615  cantnffval2  9616  cnfcom3clem  9626  ssttrcl  9636  r1fin  9697  hta  9821  infxpenlem  9935  alephon  9991  alephfplem1  10026  dfac5lem4  10048  dfac5lem5  10049  dfac5lem4OLD  10050  kmlem10  10082  fin1a2lem10  10331  fin1a2lem12  10333  hsmexlem9  10347  axcc2lem  10358  domtriomlem  10364  axdc2lem  10370  axcclem  10379  brdom7disj  10453  brdom6disj  10454  iundom2g  10462  konigthlem  10491  canthwelem  10573  wunex2  10661  wunex3  10664  1nq  10851  1pr  10938  nrex1  10987  axcnex  11070  ax1cn  11072  pnfex  11197  mnfxr  11201  cju  12153  nnexALT  12159  2nn  12230  2re  12231  2cn  12232  3nn  12236  3re  12237  3cn  12238  4nn  12240  4re  12241  4cn  12242  5nn  12243  5re  12244  5cn  12245  6nn  12246  6re  12247  6cn  12248  7nn  12249  7re  12250  7cn  12251  8nn  12252  8re  12253  8cn  12254  9nn  12255  9re  12256  9cn  12257  nn0ex  12419  zexALT  12520  nneo  12588  zeo  12590  deccl  12634  10re  12638  decnncl  12639  numnncl2  12642  decnncl2  12643  numsucc  12659  numma2c  12665  numadd  12666  numaddc  12667  nummul1c  12668  nummul2c  12669  decmul1  12683  qexALT  12889  xrex  12912  xnegex  13135  xnegcl  13140  ixxssxr  13285  fz0to4untppr  13558  fz0to5un2tp  13559  om2uzuzi  13884  ltweuz  13896  axdc4uzlem  13918  seqex  13938  seqexw  13952  m1expcl2  14020  faccl  14218  facwordi  14224  faclbnd2  14226  bccl  14257  hashen1  14305  hashrabrsn  14307  hashunlei  14360  hashpw  14371  tpf1o  14436  s1cli  14541  ccat2s1p1  14565  cats1un  14656  revs1  14700  cshwsexa  14759  cats1cli  14792  cats1fvn  14793  crre  15049  remim  15052  climmpt  15506  sumex  15623  supcvg  15791  geo2lim  15810  prodex  15840  bpoly4  15994  ere  16024  eftlub  16046  efsep  16047  tan0  16088  ef01bndlem  16121  nn0o  16322  divalglem5  16336  divalglem9  16340  sadcf  16392  smupf  16417  crth  16717  phimullem  16718  pczpre  16787  pockthi  16847  prmreclem2  16857  igz  16874  0ramcl  16963  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  strle1  17097  ndxarg  17135  basendxnn  17158  plusgndxnn  17217  tsetndxnn  17286  plendxnn  17300  dsndxnn  17319  unifndxnn  17329  prdsbasex  17382  prdsds  17396  yonedalem3  18215  isposix  18259  chnub  18557  plusffval  18583  issubmgm2  18640  efmnd1hash  18829  efmnd2hash  18831  smndex1bas  18843  smndex1sgrp  18845  smndex1mnd  18847  smndex1id  18848  smndex2dbas  18851  smndex2hbas  18853  grpsubfval  18925  mulgfval  19011  symg1hash  19331  symg2hash  19333  symgvalstruct  19338  symgfisg  19409  psgnsn  19461  psgnprfval1  19463  odfval  19473  sylow2alem2  19559  efgsval2  19674  efgsp1  19678  pgpfaclem1  20024  dvdsrval  20309  isirred  20367  scaffval  20843  cnfldex  21324  xrsex  21351  pzriprnglem4  21451  pzriprnglem5  21452  pzriprnglem6  21453  pzriprng1ALT  21463  znle  21503  znidomb  21528  cnmsgnsubg  21544  refld  21586  ipffval  21615  psrbag0  22029  psrbagsn  22030  psr1baslem  22137  mat1dimbas  22428  mat1dimscm  22431  mat1f1o  22434  mat1rhmelval  22436  m2detleib  22587  pmatcoe1fsupp  22657  indistopon  22957  iccordt  23170  conncompid  23387  ptbasfi  23537  ptcmpfi  23769  ustfn  24158  ust0  24176  ustn0  24177  tmslem  24438  nmfval  24544  cnbl0  24729  cnopn  24742  remet  24746  re2ndc  24757  zcld  24770  icccmp  24782  xrge0gsumle  24790  xrge0tsms  24791  xmetdcn  24795  divcnOLD  24825  divcn  24827  expcn  24831  expcnOLD  24833  iiconn  24848  idcncf  24879  cnmpopc  24890  cnrehmeo  24919  cnrehmeoOLD  24920  cnheiborlem  24921  rellycmp  24924  bndth  24925  evth2  24927  cnrlmod  25111  cnrlvec  25112  cncmet  25290  ishl2  25338  ehleudis  25386  ehleudisval  25387  finiunmbl  25513  ioombl1lem4  25530  vitalilem4  25580  vitalilem5  25581  ismbf2d  25609  mbfimaopnlem  25624  mbfi1fseqlem6  25689  itgex  25739  bddmulibl  25808  ditgex  25821  recnperf  25874  dvcnvrelem2  25991  ftc1  26017  mdegcl  26042  plyeq0lem  26183  aaliou3lem4  26322  dvradcnv  26398  sincn  26422  coscn  26423  tanabsge  26483  circsubm  26530  reloggim  26576  logcn  26624  dvloglem  26625  logdmopn  26626  dvlog2  26630  2irrexpq  26708  cxpcn  26722  cxpcnOLD  26723  cxpcn3  26726  resqrtcn  26727  2logb9irrALT  26776  2irrexpqALT  26778  atanrecl  26889  atan1  26906  atansopn  26910  birthdaylem1  26929  birthday  26932  emcllem4  26977  emcllem6  26979  lgamgulmlem6  27012  basellem6  27064  ppiublem1  27181  bposlem6  27268  bposlem8  27270  lgslem4  27279  lgsdir2lem2  27305  selberglem1  27524  selberglem3  27526  selberg  27527  selbergs  27553  qdrng  27599  0no  27817  1no  27818  lrrecse  27950  precsexlem11  28225  seqsex  28293  nnsex  28326  n0bday  28360  n0subs  28371  n0p1nns  28379  dfnns2  28380  zsex  28388  bdayfinbndlem1  28475  z12sex  28482  z12shalf  28488  edgfndxnn  29077  structvtxvallem  29105  usgrexmpllem  29345  usgrexmpl  29348  uhgrspan1  29388  upgrres  29391  umgrres  29392  usgrres  29393  upgrres1  29398  umgrres1  29399  usgrres1  29400  fusgrfis  29415  cusgrres  29534  vtxdlfgrval  29571  vtxdusgr0edgnelALT  29582  umgr2v2e  29611  vtxdginducedm1lem1  29625  vtxdginducedm1fi  29630  finsumvtxdg2ssteplem4  29634  pthdlem1  29851  crctcshlem3  29904  2wlkd  30021  2wlkond  30022  2trlond  30024  2pthd  30025  2pthond  30027  umgr2adedgwlkonALT  30032  0pth  30212  wlk2v2e  30244  3wlkd  30257  3trlond  30260  3pthd  30261  3pthond  30262  3spthond  30264  eupthvdres  30322  eulerpathpr  30327  konigsbergumgr  30338  konigsberglem5  30343  konigsberg  30344  ex-lcm  30545  isvciOLD  30668  isnvi  30701  blocni  30893  hmoval  30898  cncph  30907  ipasslem7  30924  siilem2  30940  normlem2  31199  normlem3  31200  normlem6  31203  h0elch  31343  hhssabloilem  31349  hhsssh  31357  spansnji  31734  nonbooli  31739  3oalem5  31754  3oalem6  31755  3oai  31756  mayetes3i  31817  nmcexi  32114  nmbdfnlb  32138  rnelshi  32147  cnlnadjlem5  32159  pjbdlni  32237  golem2  32360  goeqi  32361  dp2clq  32973  rpdp2cl  32974  rpdp2cl2  32975  dpmul100  32989  rpdpcl  32995  xrge0tsmsd  33167  pmtrto1cl  33193  psgnfzto1stlem  33194  fzto1st  33197  psgnfzto1st  33199  nn0omnd  33437  xrge0slmod  33441  qusima  33501  prmidl0  33543  fply1  33651  extvfvcl  33713  ply1degltdimlem  33800  ccfldextdgrr  33850  algextdeglem8  33902  constrfin  33924  2sqr3minply  33958  2sqr3nconstr  33959  cos9thpiminplylem4  33963  cos9thpiminplylem5  33964  cos9thpinconstrlem2  33968  circtopn  34015  circcn  34016  zarcmplem  34059  tpr2tp  34082  tpr2rico  34090  ordtprsval  34096  ordtprsuni  34097  ordtrestNEW  34099  ordtrest2NEWlem  34100  ordtrest2NEW  34101  ordtconnlem1  34102  mndpluscn  34104  xrge0pluscn  34118  xrge0mulc1cn  34119  xrge0haus  34122  lmlimxrge0  34126  lmxrge0  34130  qqhcn  34169  qqhucn  34170  esumex  34207  esumcst  34241  hasheuni  34263  esumcvg  34264  prsiga  34309  brsiga  34361  mbfmcnt  34446  sxbrsigalem3  34450  dya2iocuni  34461  dya2iocucvr  34462  sxbrsigalem1  34463  sxbrsiga  34468  eulerpartlemt  34549  fibp1  34579  coinflipprob  34658  coinfliprv  34661  ccatmulgnn0dir  34720  signswplusg  34733  hgt750lem2  34830  hgt750leme  34836  bnj105  34901  bnj918  34943  bnj95  35040  bnj852  35097  bnj865  35099  fineqvnttrclse  35302  subfacp1lem1  35395  subfacp1lem3  35398  subfacp1lem5  35400  subfacp1lem6  35401  kur14lem7  35428  iisconn  35468  iillysconn  35469  cvmliftlem5  35505  cvmliftlem8  35508  cvmliftlem10  35510  cvmlift2lem9  35527  satfv0  35574  goalrlem  35612  goalr  35613  satffunlem2lem2  35622  circum  35890  iexpire  35951  altopex  36176  colinearex  36276  ssoninhaus  36664  cnndvlem2  36760  bj-prex  37288  bj-prfromadj  37293  bj-pinftyccb  37476  taupi  37578  isbasisrelowl  37613  relowlpssretop  37619  poimirlem29  37900  poimirlem30  37901  poimirlem31  37902  dvasin  37955  dvacos  37956  areacirc  37964  upixp  37980  fdc  37996  lmclim2  38009  cncfres  38016  heibor1lem  38060  rrnval  38078  rrnmet  38080  reheibor  38090  isdrngo2  38209  isrngohom  38216  idlval  38264  isidl  38265  igenval  38312  scottexf  38419  cnvepresex  38587  preex  38743  renegclALT  39339  ldualfvadd  39504  cmtfvalN  39586  cvrfval  39644  cdleme31fv  40766  cdlemk40  41293  cdlemk56  41347  dibopelvalN  41519  dibopelval2  41521  dibelval3  41523  diblsmopel  41547  cdlemn11a  41583  dihopelvalcpre  41624  dihpN  41712  hlhilsca  42311  hlhilip  42324  3factsumint1  42391  lcmineqlem23  42421  aks4d1p1p6  42443  aks4d1p1p5  42445  aks6d1c6isolem2  42545  itrere  42688  acos1half  42728  redvmptabs  42730  readvrec2  42731  sn-0tie0  42821  sn-itrere  42858  sn-retire  42859  prjspval  42961  flt4lem5e  43014  sn-isghm  43031  mapfzcons2  43076  jm2.23  43353  jm2.27dlem2  43367  jm2.27dlem4  43369  rmydioph  43371  rmxdioph  43373  expdiophlem2  43379  expdioph  43380  aomclem6  43416  pwslnmlem0  43448  frlmpwfi  43455  mncn0  43496  aaitgo  43519  arearect  43572  areaquad  43573  omcl3g  43691  comptiunov2i  44062  frege110  44329  frege133  44352  scottex2  44601  radcnvrat  44670  uzmptshftfval  44702  dvradcnv2  44703  binomcxplemdvbinom  44709  binomcxplemcvg  44710  binomcxplemnotnn0  44712  permaxinf2lem  45368  rfcnpre1  45379  fcnre  45385  refsumcn  45390  refsum2cnlem1  45397  unirnmapsn  45572  infxrpnf  45804  iocopn  45880  icoopn  45885  mccl  45958  clim1fr1  45961  islptre  45979  sumnnodd  45990  lptre2pt  45998  limclner  46009  limclr  46013  expfac  46015  0cnf  46235  icccncfext  46245  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  itgsin0pilem1  46308  iblempty  46323  itgvol0  46326  stoweidlem47  46405  stoweidlem53  46411  stoweidlem57  46415  stoweidlem59  46417  wallispilem3  46425  wallispilem4  46426  wallispilem5  46427  wallispi  46428  stirlinglem1  46432  stirlinglem8  46439  stirlinglem12  46443  stirlinglem13  46444  stirlinglem14  46445  stirlinglem15  46446  dirkerper  46454  dirkercncflem2  46462  fourierdlem16  46481  fourierdlem21  46486  fourierdlem22  46487  fourierdlem36  46501  fourierdlem42  46507  fourierdlem71  46535  fourierdlem83  46547  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  fourierdlem112  46576  fourierdlem114  46578  sqwvfoura  46586  sqwvfourb  46587  fourierswlem  46588  fouriersw  46589  etransclem48  46640  salexct3  46700  salgencntex  46701  salgensscntex  46702  iooborel  46709  bor1sal  46713  gsumge0cl  46729  sge0tsms  46738  sge0isum  46785  nnfoctbdjlem  46813  isomenndlem  46888  mbfresmf  47097  incsmflem  47099  incsmf  47100  smfmbfcex  47118  decsmflem  47124  decsmf  47125  smflimlem1  47129  smfpimbor1lem2  47157  smf2id  47159  smfco  47160  smfpimcclem  47165  lambert0  47247  sprsymrelfolem1  47852  sprbisymrel  47859  fmtno0prm  47918  fmtno1prm  47919  fmtno2prm  47920  fmtno3prm  47922  fmtno4prm  47935  m2prm  47951  m3prm  47952  m5prm  47958  m7prm  47960  lighneallem4a  47968  0evenALTV  48048  1oddALTV  48050  2evenALTV  48052  6even  48071  7odd  48072  8even  48073  9gbo  48134  opstrgric  48286  ushggricedg  48287  grtri  48300  usgrexmpl1  48382  usgrexmpl1vtx  48383  usgrexmpl1edg  48384  usgrexmpl2  48387  usgrexmpl2vtx  48388  usgrexmpl2edg  48389  gpgprismgr4cycllem5  48459  pgnbgreunbgr  48485  pgn4cyclex  48486  uspgrex  48510  lmod1zrnlvec  48854  zlmodzxzldeplem1  48860  zlmodzxzldeplem3  48862  zlmodzxzldeplem4  48863  zlmodzxzldep  48864  ldepsnlinclem1  48865  ldepsnlinclem2  48866  blennn0elnn  48937  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  itcovalpclem2  49031  itcovalt2lem2  49036  ackval42  49056  rrx2line  49100  rrx2linesl  49103  spheres  49106  2sphere  49109  2sphere0  49110  line2x  49114  line2y  49115  resipos  49334  functhinclem1  49803  prsthinc  49823  setc1oterm  49850  funcsetc1ocl  49855  funcsetc1o  49856  isinito2lem  49857  isinito3  49859  functermc2  49868  incat  49960  setc1onsubc  49961