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 230	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eqeltrri  2831  3eltr4i  2847  intab  4983  axrep6g  5294  unisn2  5313  inex2  5319  vpwex  5376  ord3ex  5386  zfpair  5420  vsnex  5430  opex  5465  otex  5466  uniopel  5517  elvvuni  5753  isarep2  6640  fvex  6905  fvexi  6906  riotaex  7369  ovexi  7443  tpex  7734  oprabex  7963  oprabrexex2  7965  mpoexw  8065  mptmpoopabbrd  8067  tfrlem16  8393  1oex  8476  2oex  8477  1on  8478  1onOLD  8479  2on  8480  2onOLD  8481  3on  8484  4on  8485  2oexOLD  8487  oesuclem  8525  oecl  8537  o2p2e4  8541  nnecl  8613  1onnALT  8640  2onnALT  8642  3onn  8643  4onn  8644  mapsnf1o2  8888  sbthlem10  9092  imafi  9175  pwfi  9178  cnvfi  9180  fnfi  9181  nnunifi  9294  xpfiOLD  9318  prfi  9322  tpfi  9323  pwfiOLD  9347  fczfsuppd  9381  cantnfvalf  9660  oemapwe  9689  cantnffval2  9690  cnfcom3clem  9700  ssttrcl  9710  r1fin  9768  hta  9892  infxpenlem  10008  alephon  10064  alephfplem1  10099  dfac5lem4  10121  dfac5lem5  10122  kmlem10  10154  fin1a2lem10  10404  fin1a2lem12  10406  hsmexlem9  10420  axcc2lem  10431  domtriomlem  10437  axdc2lem  10443  axcclem  10452  brdom7disj  10526  brdom6disj  10527  iundom2g  10535  konigthlem  10563  canthwelem  10645  wunex2  10733  wunex3  10736  1nq  10923  1pr  11010  nrex1  11059  axcnex  11142  ax1cn  11144  pnfex  11267  mnfxr  11271  inelr  12202  cju  12208  nnexALT  12214  2nn  12285  2re  12286  2cn  12287  3nn  12291  3re  12292  3cn  12293  4nn  12295  4re  12296  4cn  12297  5nn  12298  5re  12299  5cn  12300  6nn  12301  6re  12302  6cn  12303  7nn  12304  7re  12305  7cn  12306  8nn  12307  8re  12308  8cn  12309  9nn  12310  9re  12311  9cn  12312  nn0ex  12478  zexALT  12578  nneo  12646  zeo  12648  deccl  12692  10re  12696  decnncl  12697  numnncl2  12700  decnncl2  12701  numsucc  12717  numma2c  12723  numadd  12724  numaddc  12725  nummul1c  12726  nummul2c  12727  decmul1  12741  qexALT  12948  xrex  12971  xnegex  13187  xnegcl  13192  ixxssxr  13336  om2uzuzi  13914  ltweuz  13926  axdc4uzlem  13948  seqex  13968  seqexw  13982  m1expcl2  14051  faccl  14243  facwordi  14249  faclbnd2  14251  bccl  14282  hashen1  14330  hashrabrsn  14332  hashunlei  14385  hashpw  14396  s1cli  14555  ccat2s1p1  14579  cats1un  14671  revs1  14715  cshwsexa  14774  cshwsexaOLD  14775  cats1cli  14808  cats1fvn  14809  crre  15061  remim  15064  climmpt  15515  sumex  15634  supcvg  15802  geo2lim  15821  prodex  15851  bpoly4  16003  ere  16032  eftlub  16052  efsep  16053  tan0  16094  ef01bndlem  16127  nn0o  16326  divalglem5  16340  divalglem9  16344  sadcf  16394  smupf  16419  crth  16711  phimullem  16712  pczpre  16780  pockthi  16840  prmreclem2  16850  igz  16867  0ramcl  16956  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  strle1  17091  ndxarg  17129  basendxnn  17154  basendxnnOLD  17155  plusgndxnn  17225  tsetndxnn  17299  plendxnn  17313  dsndxnn  17332  unifndxnn  17342  prdsbasex  17396  prdsds  17410  yonedalem3  18233  isposix  18278  isposixOLD  18279  plusffval  18567  efmnd1hash  18773  efmnd2hash  18775  smndex1bas  18787  smndex1sgrp  18789  smndex1mnd  18791  smndex1id  18792  smndex2dbas  18795  smndex2hbas  18797  grpsubfval  18868  mulgfval  18952  symg1hash  19257  symg2hash  19259  symgvalstruct  19264  symgvalstructOLD  19265  symgfisg  19336  psgnsn  19388  psgnprfval1  19390  odfval  19400  sylow2alem2  19486  efgsval2  19601  efgsp1  19605  pgpfaclem1  19951  dvdsrval  20175  isirred  20233  scaffval  20490  xrsex  20960  zlmlemOLD  21067  znle  21088  znidomb  21117  cnmsgnsubg  21130  refld  21172  ipffval  21201  psrbag0  21623  psrbagsn  21624  psr1baslem  21709  mat1dimbas  21974  mat1dimscm  21977  mat1f1o  21980  mat1rhmelval  21982  m2detleib  22133  pmatcoe1fsupp  22203  indistopon  22504  iccordt  22718  conncompid  22935  ptbasfi  23085  ptcmpfi  23317  ustfn  23706  ust0  23724  ustn0  23725  tmslem  23990  tmslemOLD  23991  nmfval  24097  tnglemOLD  24150  cnbl0  24290  cnopn  24303  remet  24306  re2ndc  24317  zcld  24329  icccmp  24341  xrge0gsumle  24349  xrge0tsms  24350  xmetdcn  24354  divcn  24384  expcn  24388  iiconn  24403  idcncf  24434  cnmpopc  24444  cnrehmeo  24469  cnheiborlem  24470  rellycmp  24473  bndth  24474  evth2  24476  cnrlmod  24659  cnrlvec  24660  cncmet  24839  ishl2  24887  ehleudis  24935  ehleudisval  24936  finiunmbl  25061  ioombl1lem4  25078  vitalilem4  25128  vitalilem5  25129  ismbf2d  25157  mbfimaopnlem  25172  mbfi1fseqlem6  25238  itgex  25288  bddmulibl  25356  ditgex  25369  recnperf  25422  dvcnvrelem2  25535  ftc1  25559  mdegcl  25587  plyeq0lem  25724  aaliou3lem4  25859  dvradcnv  25933  sincn  25956  coscn  25957  tanabsge  26016  circsubm  26062  reloggim  26107  logcn  26155  dvloglem  26156  logdmopn  26157  dvlog2  26161  2irrexpq  26239  cxpcn  26253  cxpcn3  26256  resqrtcn  26257  2logb9irrALT  26303  2irrexpqALT  26305  atanrecl  26416  atan1  26433  atansopn  26437  birthdaylem1  26456  birthday  26459  emcllem4  26503  emcllem6  26505  lgamgulmlem6  26538  basellem6  26590  ppiublem1  26705  bposlem6  26792  bposlem8  26794  lgslem4  26803  lgsdir2lem2  26829  selberglem1  27048  selberglem3  27050  selberg  27051  selbergs  27077  qdrng  27123  0sno  27327  1sno  27328  lrrecse  27426  precsexlem11  27663  edgfndxnn  28250  structvtxvallem  28280  usgrexmpllem  28517  usgrexmpl  28520  uhgrspan1  28560  upgrres  28563  umgrres  28564  usgrres  28565  upgrres1  28570  umgrres1  28571  usgrres1  28572  fusgrfis  28587  cusgrres  28705  vtxdlfgrval  28742  vtxdusgr0edgnelALT  28753  umgr2v2e  28782  vtxdginducedm1lem1  28796  vtxdginducedm1fi  28801  finsumvtxdg2ssteplem4  28805  pthdlem1  29023  crctcshlem3  29073  2wlkd  29190  2wlkond  29191  2trlond  29193  2pthd  29194  2pthond  29196  umgr2adedgwlkonALT  29201  0pth  29378  wlk2v2e  29410  3wlkd  29423  3trlond  29426  3pthd  29427  3pthond  29428  3spthond  29430  eupthvdres  29488  eulerpathpr  29493  konigsbergumgr  29504  konigsberglem5  29509  konigsberg  29510  ex-lcm  29711  isvciOLD  29833  isnvi  29866  blocni  30058  hmoval  30063  cncph  30072  ipasslem7  30089  siilem2  30105  normlem2  30364  normlem3  30365  normlem6  30368  h0elch  30508  hhssabloilem  30514  hhsssh  30522  spansnji  30899  nonbooli  30904  3oalem5  30919  3oalem6  30920  3oai  30921  mayetes3i  30982  nmcexi  31279  nmbdfnlb  31303  rnelshi  31312  cnlnadjlem5  31324  pjbdlni  31402  golem2  31525  goeqi  31526  dp2clq  32047  rpdp2cl  32048  rpdp2cl2  32049  dpmul100  32063  rpdpcl  32069  xrge0tsmsd  32209  pmtrto1cl  32258  psgnfzto1stlem  32259  fzto1st  32262  psgnfzto1st  32264  nn0omnd  32460  xrge0slmod  32463  qusima  32519  prmidl0  32569  fply1  32637  ply1degltdimlem  32707  ccfldextdgrr  32746  circtopn  32817  circcn  32818  zarcmplem  32861  tpr2tp  32884  tpr2rico  32892  ordtprsval  32898  ordtprsuni  32899  ordtrestNEW  32901  ordtrest2NEWlem  32902  ordtrest2NEW  32903  ordtconnlem1  32904  mndpluscn  32906  xrge0pluscn  32920  xrge0mulc1cn  32921  xrge0haus  32924  lmlimxrge0  32928  lmxrge0  32932  qqhcn  32971  qqhucn  32972  esumex  33027  esumcst  33061  hasheuni  33083  esumcvg  33084  prsiga  33129  brsiga  33181  mbfmcnt  33267  sxbrsigalem3  33271  dya2iocuni  33282  dya2iocucvr  33283  sxbrsigalem1  33284  sxbrsiga  33289  eulerpartlemt  33370  fibp1  33400  coinflipprob  33478  coinfliprv  33481  ccatmulgnn0dir  33553  signswplusg  33566  hgt750lem2  33664  hgt750leme  33670  bnj105  33735  bnj918  33777  bnj95  33875  bnj852  33932  bnj865  33934  subfacp1lem1  34170  subfacp1lem3  34173  subfacp1lem5  34175  subfacp1lem6  34176  kur14lem7  34203  iisconn  34243  iillysconn  34244  cvmliftlem5  34280  cvmliftlem8  34283  cvmliftlem10  34285  cvmlift2lem9  34302  satfv0  34349  goalrlem  34387  goalr  34388  satffunlem2lem2  34397  circum  34659  iexpire  34705  altopex  34932  colinearex  35032  gg-divcn  35163  gg-expcn  35164  gg-cnrehmeo  35171  gg-cnfldex  35180  gg-cxpcn  35184  ssoninhaus  35333  cnndvlem2  35414  bj-prex  35921  bj-prfromadj  35926  bj-pinftyccb  36102  taupi  36204  isbasisrelowl  36239  relowlpssretop  36245  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  dvasin  36572  dvacos  36573  areacirc  36581  upixp  36597  fdc  36613  lmclim2  36626  cncfres  36633  heibor1lem  36677  rrnval  36695  rrnmet  36697  reheibor  36707  isdrngo2  36826  isrngohom  36833  idlval  36881  isidl  36882  igenval  36929  scottexf  37036  cnvepresex  37203  renegclALT  37833  ldualfvadd  37998  cmtfvalN  38080  cvrfval  38138  cdleme31fv  39261  cdlemk40  39788  cdlemk56  39842  dibopelvalN  40014  dibopelval2  40016  dibelval3  40018  diblsmopel  40042  cdlemn11a  40078  dihopelvalcpre  40119  dihpN  40207  hlhilsca  40806  hlhilip  40823  3factsumint1  40886  lcmineqlem23  40916  aks4d1p1p6  40938  aks4d1p1p5  40940  sn-0tie0  41312  itrere  41339  retire  41340  prjspval  41345  flt4lem5e  41398  acos1half  41415  mapfzcons2  41457  jm2.23  41735  jm2.27dlem2  41749  jm2.27dlem4  41751  rmydioph  41753  rmxdioph  41755  expdiophlem2  41761  expdioph  41762  aomclem6  41801  pwslnmlem0  41833  frlmpwfi  41840  mncn0  41881  aaitgo  41904  arearect  41964  areaquad  41965  omcl3g  42084  comptiunov2i  42457  frege110  42724  frege133  42747  scottex2  43004  radcnvrat  43073  uzmptshftfval  43105  dvradcnv2  43106  binomcxplemdvbinom  43112  binomcxplemcvg  43113  binomcxplemnotnn0  43115  rfcnpre1  43703  fcnre  43709  refsumcn  43714  refsum2cnlem1  43721  unirnmapsn  43913  infxrpnf  44156  iocopn  44233  icoopn  44238  mccl  44314  clim1fr1  44317  islptre  44335  sumnnodd  44346  lptre2pt  44356  limclner  44367  limclr  44371  expfac  44373  0cnf  44593  icccncfext  44603  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  itgsin0pilem1  44666  iblempty  44681  itgvol0  44684  stoweidlem47  44763  stoweidlem53  44769  stoweidlem57  44773  stoweidlem59  44775  wallispilem3  44783  wallispilem4  44784  wallispilem5  44785  wallispi  44786  stirlinglem1  44790  stirlinglem8  44797  stirlinglem12  44801  stirlinglem13  44802  stirlinglem14  44803  stirlinglem15  44804  dirkerper  44812  dirkercncflem2  44820  fourierdlem16  44839  fourierdlem21  44844  fourierdlem22  44845  fourierdlem36  44859  fourierdlem42  44865  fourierdlem71  44893  fourierdlem83  44905  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fourierdlem112  44934  fourierdlem114  44936  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  etransclem48  44998  salexct3  45058  salgencntex  45059  salgensscntex  45060  iooborel  45067  bor1sal  45071  gsumge0cl  45087  sge0tsms  45096  sge0isum  45143  nnfoctbdjlem  45171  isomenndlem  45246  mbfresmf  45455  incsmflem  45457  incsmf  45458  smfmbfcex  45476  decsmflem  45482  decsmf  45483  smflimlem1  45487  smfpimbor1lem2  45515  smf2id  45517  smfco  45518  smfpimcclem  45523  tworepnotupword  45600  sprsymrelfolem1  46160  sprbisymrel  46167  fmtno0prm  46226  fmtno1prm  46227  fmtno2prm  46228  fmtno3prm  46230  fmtno4prm  46243  m2prm  46259  m3prm  46260  m5prm  46266  m7prm  46268  lighneallem4a  46276  0evenALTV  46356  1oddALTV  46358  2evenALTV  46360  6even  46379  7odd  46380  8even  46381  9gbo  46442  strisomgrop  46508  ushrisomgr  46509  uspgrex  46528  issubmgm2  46560  pzriprnglem4  46808  pzriprnglem5  46809  pzriprnglem6  46810  pzriprng1ALT  46820  lmod1zrnlvec  47175  zlmodzxzldeplem1  47181  zlmodzxzldeplem3  47183  zlmodzxzldeplem4  47184  zlmodzxzldep  47185  ldepsnlinclem1  47186  ldepsnlinclem2  47187  blennn0elnn  47263  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  itcovalpclem2  47357  itcovalt2lem2  47362  ackval42  47382  rrx2line  47426  rrx2linesl  47429  spheres  47432  2sphere  47435  2sphere0  47436  line2x  47440  line2y  47441  functhinclem1  47661  prsthinc  47674