Theorem eqeltri 2881

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

Syntax hints:   = wceq 1637   ∈ wcel 2156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-clel 2802

This theorem is referenced by:  eqeltrri  2882  3eltr4i  2898  intab  4699  unisn2  4989  inex2  4995  vpwex  5047  ord3ex  5056  zfpair  5094  opex  5122  otex  5123  uniopel  5171  elvvuni  5379  predasetex  5908  isarep2  6189  fvex  6421  fvexi  6422  riotaex  6839  ovexi  6907  tpex  7187  abrexex2OLD  7380  oprabex  7386  oprabrexex2  7388  tfrlem16  7725  1on  7803  2on  7805  3on  7807  4on  7808  oesuclem  7842  oecl  7854  nnecl  7930  1onn  7956  2onn  7957  3onn  7958  4onn  7959  mapsnf1o2  8142  sbthlem10  8318  nnunifi  8450  xpfi  8470  prfi  8474  tpfi  8475  fnfi  8477  pwfi  8500  fczfsuppd  8532  inf0  8765  cantnfvalf  8809  oemapwe  8838  cantnffval2  8839  cnfcom3clem  8849  r1fin  8883  hta  9007  infxpenlem  9119  alephon  9175  alephfplem1  9210  dfac5lem4  9232  dfac5lem5  9233  kmlem10  9266  fin1a2lem10  9516  fin1a2lem12  9518  hsmexlem9  9532  axcc2lem  9543  domtriomlem  9549  axdc2lem  9555  axcclem  9564  brdom7disj  9638  brdom6disj  9639  iundom2g  9647  konigthlem  9675  canthwelem  9757  wunex2  9845  wunex3  9848  1nq  10035  1pr  10122  axcnex  10253  ax1cn  10255  pnfxr  10377  mnfxr  10381  inelr  11295  cju  11301  nnexALT  11307  2re  11374  3re  11378  4re  11381  5re  11383  6re  11385  7re  11387  8re  11389  9re  11391  2nn  11462  3nn  11463  4nn  11464  5nn  11465  6nn  11466  7nn  11467  8nn  11468  9nn  11469  nn0ex  11565  zexALT  11662  nneo  11727  zeo  11729  deccl  11774  decnncl  11779  numnncl2  11782  decnncl2  11783  numsucc  11799  numma2c  11805  numadd  11806  numaddc  11807  nummul1c  11808  nummul2c  11809  qexALT  12022  xrex  12043  xnegex  12257  xnegcl  12262  ixxssxr  12405  om2uzuzi  12972  ltweuz  12984  axdc4uzlem  13006  seqex  13026  m1expcl2  13105  faccl  13290  facwordi  13296  faclbnd2  13298  bccl  13329  hashen1  13378  hashrabrsn  13379  hashunlei  13429  hashpw  13440  s1cli  13600  cats1un  13699  revs1  13738  cshwsexa  13794  cats1cli  13826  cats1fvn  13827  crre  14077  remim  14080  climmpt  14525  sumex  14641  supcvg  14810  geo2lim  14828  prodex  14858  bpoly4  15010  ere  15039  eftlub  15059  efsep  15060  tan0  15101  ef01bndlem  15134  nn0o  15319  divalglem5  15340  divalglem9  15344  sadcf  15394  smupf  15419  crth  15700  phimullem  15701  eulerthlem2  15704  pczpre  15769  pockthi  15828  prmreclem2  15838  igz  15855  0ramcl  15944  1259lem1  16049  1259lem2  16050  1259lem3  16051  1259lem4  16052  1259lem5  16053  1259prm  16054  2503lem1  16055  2503lem2  16056  2503lem3  16057  2503prm  16058  4001lem1  16059  4001lem2  16060  4001lem3  16061  4001lem4  16062  4001prm  16063  ndxarg  16093  basendxnn  16135  ressval3dOLD  16149  strle1  16184  prdsbasex  16316  prdsds  16329  subccatid  16710  funcres2c  16765  ressffth  16802  fuccofval  16823  fuchom  16825  fuccatid  16833  xpccatid  17033  yonedalem3  17125  isposix  17162  plusffval  17452  eqgen  17849  orbsta  17947  symg1hash  18016  symg2hash  18018  symgfisg  18089  psgnsn  18141  psgnprfval1  18143  sylow2alem2  18234  sylow2blem1  18236  sylow2blem2  18237  efgsval2  18347  efgsp1  18351  frgpnabllem1  18477  gsummptnn0fzOLD  18584  dvdsrval  18847  isirred  18901  scaffval  19085  subrgmvr  19670  opsrle  19684  psrbag0  19702  psrbagsn  19703  subrgascl  19706  psr1baslem  19763  evl1fval  19900  xrsex  19969  zlmlem  20073  znle  20092  znbas  20099  znzrhval  20102  znidomb  20117  cnmsgnsubg  20130  relt  20170  retos  20173  refld  20174  ipffval  20203  frlmlbs  20346  lsslindf  20379  lsslinds  20380  uvcendim  20396  matgsum  20453  matmulr  20454  mat1dimbas  20489  mat1dimscm  20492  mat1f1o  20495  mat1rhmelval  20497  scmatghm  20550  marepvfval  20582  m2detleib  20648  pmatcoe1fsupp  20719  m2cpmmhm  20763  cpm2mfval  20767  cpmadumatpolylem2  20900  indistopon  21019  iccordt  21232  conncompid  21448  ptbasfi  21598  ptcmpfi  21830  cldsubg  22127  ustfn  22218  ust0  22236  ustn0  22237  tmslem  22500  nmfval  22606  tnglem  22657  cnbl0  22790  cnopn  22803  remet  22806  re2ndc  22817  zcld  22829  icccmp  22841  xrge0gsumle  22849  xrge0tsms  22850  xmetdcn  22854  divcn  22884  expcn  22888  iiconn  22903  cnmpt2pc  22940  cnrehmeo  22965  cnheiborlem  22966  rellycmp  22969  bndth  22970  evth2  22972  pi1bas  23050  cnrlmod  23155  cnrlvec  23156  cncmet  23331  ishl2  23378  finiunmbl  23525  ioombl1lem4  23542  vitalilem4  23592  vitalilem5  23593  ismbf2d  23621  mbfimaopnlem  23636  mbfi1fseqlem6  23701  itgex  23751  bddmulibl  23819  ditgex  23830  recnperf  23883  dv11cn  23978  dvcnvrelem2  23995  ftc1  24019  mdegcl  24043  plyeq0lem  24180  quotval  24261  aaliou3lem4  24315  dvradcnv  24389  pserdvlem2  24396  sincn  24412  coscn  24413  tanabsge  24473  circsubm  24514  reloggim  24559  logcn  24607  dvloglem  24608  logdmopn  24609  dvlog2  24613  cxpcn  24700  cxpcn3  24703  resqrtcn  24704  ang180lem3  24755  atanrecl  24852  atan1  24869  atansopn  24873  birthdaylem1  24892  birthday  24895  emcllem4  24939  emcllem6  24941  lgamgulmlem6  24974  basellem6  25026  ppiublem1  25141  dchrptlem2  25204  bposlem6  25228  bposlem8  25230  lgslem4  25239  lgsdir2lem2  25265  selberglem1  25448  selberglem3  25450  selberg  25451  selbergs  25477  qdrng  25523  edgfndxnn  26084  structvtxvallem  26123  usgrexmpllem  26368  usgrexmpl  26371  uhgrspan1  26411  upgrres  26414  umgrres  26415  usgrres  26416  upgrres1  26421  umgrres1  26422  usgrres1  26423  nbusgrf1o1  26488  uvtxavalOLD  26506  uvtxa01vtx0OLD  26520  cusgrres  26572  vtxdlfgrval  26609  vtxdusgr0edgnelALT  26620  umgr2v2e  26649  vtxdginducedm1lem1  26663  vtxdginducedm1lem4  26666  vtxdginducedm1fi  26668  finsumvtxdg2ssteplem4  26672  pthdlem1  26890  crctcshlem3  26940  2wlkd  27076  2wlkond  27077  2trlond  27079  2pthd  27080  2pthond  27082  umgr2adedgwlkonALT  27087  0pth  27298  wlk2v2elem2  27329  wlk2v2e  27330  3wlkd  27343  3trlond  27346  3pthd  27347  3pthond  27348  3spthond  27350  eupthvdres  27408  eulerpathpr  27413  konigsbergumgr  27424  konigsberglem5  27429  konigsberg  27430  ex-lcm  27646  isvciOLD  27763  isnvi  27796  bloval  27964  blocni  27988  hmoval  27993  cncph  28002  ipasslem7  28019  siilem2  28035  normlem2  28296  normlem3  28297  normlem6  28300  h0elch  28440  hhssabloilem  28446  hhsssh  28454  spansnji  28833  nonbooli  28838  3oalem5  28853  3oalem6  28854  3oai  28855  mayetes3i  28916  nmcexi  29213  nmbdfnlb  29237  rnelshi  29246  cnlnadjlem5  29258  pjbdlni  29336  golem2  29459  goeqi  29460  dp2clq  29914  rpdp2cl  29915  rpdp2cl2  29916  dpmul100  29930  rpdpcl  29936  xrge0tsmsd  30110  nn0omnd  30166  xrge0slmod  30169  pmtrto1cl  30174  psgnfzto1stlem  30175  fzto1st  30178  psgnfzto1st  30180  circtopn  30229  circcn  30230  tpr2tp  30275  tpr2rico  30283  ordtprsval  30289  ordtprsuni  30290  ordtrestNEW  30292  ordtrest2NEWlem  30293  ordtrest2NEW  30294  ordtconnlem1  30295  mndpluscn  30297  xrge0pluscn  30311  xrge0mulc1cn  30312  xrge0haus  30315  lmlimxrge0  30319  lmxrge0  30323  qqhcn  30360  qqhucn  30361  esumex  30416  esumcst  30450  hasheuni  30472  esumcvg  30473  isrnsigaOLD  30500  prsiga  30519  brsiga  30571  mbfmcnt  30655  sxbrsigalem3  30659  dya2iocuni  30670  dya2iocucvr  30671  sxbrsigalem1  30672  sxbrsiga  30677  eulerpartlemt  30758  fibp1  30788  coinflipprob  30866  coinfliprv  30869  ccatmulgnn0dir  30944  signswplusg  30957  hgt750lem2  31055  hgt750leme  31061  bnj105  31115  bnj918  31159  bnj95  31257  bnj852  31314  bnj865  31316  subfacp1lem1  31484  subfacp1lem3  31487  subfacp1lem5  31489  subfacp1lem6  31490  kur14lem7  31517  iisconn  31557  iillysconn  31558  cvmliftlem5  31594  cvmliftlem8  31597  cvmliftlem10  31599  cvmlift2lem9  31616  circum  31890  iexpire  31943  trpredex  32057  altopex  32388  colinearex  32488  ssoninhaus  32764  cnndvlem2  32846  bj-2ex  33249  bj-pinftyccb  33425  taupi  33486  isbasisrelowl  33522  relowlpssretop  33528  cnfin0  33556  cnfinltrel  33557  poimirlem29  33751  poimirlem30  33752  poimirlem31  33753  dvasin  33808  dvacos  33809  areacirc  33817  upixp  33836  fdc  33852  lmclim2  33865  idcncf  33870  cncfres  33875  heibor1lem  33919  rrnval  33937  rrnmet  33939  reheibor  33949  isdrngo2  34068  isrngohom  34075  idlval  34123  isidl  34124  igenval  34171  scottexf  34286  cnvepresex  34419  renegclALT  34742  ldualfvadd  34908  cmtfvalN  34990  cvrfval  35048  cdleme31fv  36171  cdlemk40  36698  cdlemk56  36752  dibopelvalN  36924  dibopelval2  36926  dibelval3  36928  diblsmopel  36952  cdlemn11a  36988  dihopelvalcpre  37029  dihpN  37117  hlhilsca  37716  hlhilip  37729  mapfzcons2  37784  jm2.23  38064  jm2.27dlem2  38078  jm2.27dlem4  38080  rmydioph  38082  rmxdioph  38084  expdiophlem2  38090  expdioph  38091  aomclem6  38130  pwslnmlem0  38162  frlmpwfi  38169  mncn0  38210  aaitgo  38233  arearect  38301  areaquad  38302  comptiunov2i  38498  frege110  38767  frege133  38790  radcnvrat  39013  uzmptshftfval  39045  dvradcnv2  39046  binomcxplemdvbinom  39052  binomcxplemcvg  39053  binomcxplemnotnn0  39055  rfcnpre1  39672  fcnre  39678  refsumcn  39683  refsum2cnlem1  39690  unirnmapsn  39893  infxrpnf  40153  iocopn  40227  icoopn  40232  mccl  40310  clim1fr1  40313  islptre  40331  sumnnodd  40342  lptre2pt  40352  limclner  40363  limclr  40367  expfac  40369  0cnf  40570  icccncfext  40580  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  itgsin0pilem1  40645  iblempty  40660  itgvol0  40663  stoweidlem47  40743  stoweidlem53  40749  stoweidlem57  40753  stoweidlem59  40755  wallispilem3  40763  wallispilem4  40764  wallispilem5  40765  wallispi  40766  stirlinglem1  40770  stirlinglem8  40777  stirlinglem12  40781  stirlinglem13  40782  stirlinglem14  40783  stirlinglem15  40784  dirkerper  40792  dirkercncflem2  40800  fourierdlem16  40819  fourierdlem21  40824  fourierdlem22  40825  fourierdlem36  40839  fourierdlem42  40845  fourierdlem71  40873  fourierdlem83  40885  fourierdlem102  40904  fourierdlem103  40905  fourierdlem104  40906  fourierdlem111  40913  fourierdlem112  40914  fourierdlem114  40916  sqwvfoura  40924  sqwvfourb  40925  fourierswlem  40926  fouriersw  40927  etransclem48  40978  salexct3  41039  salgencntex  41040  salgensscntex  41041  iooborel  41048  bor1sal  41052  gsumge0cl  41067  sge0tsms  41076  sge0isum  41123  nnfoctbdjlem  41151  isomenndlem  41226  mbfresmf  41430  incsmflem  41432  incsmf  41433  smfmbfcex  41450  decsmflem  41456  decsmf  41457  smflimlem1  41461  smfpimbor1lem2  41488  smf2id  41490  smfco  41491  smfpimcclem  41495  fmtno0prm  42045  fmtno1prm  42046  fmtno2prm  42047  fmtno3prm  42049  fmtno4prm  42062  m2prm  42080  m3prm  42081  m5prm  42088  m7prm  42091  lighneallem4a  42100  0evenALTV  42174  1oddALTV  42176  2evenALTV  42178  6even  42195  7odd  42196  8even  42197  9gbo  42237  sprsymrelfolem1  42310  sprbisymrel  42317  uspgrex  42326  issubmgm2  42358  lmod1zrnlvec  42851  zlmodzxzldeplem1  42857  zlmodzxzldeplem3  42859  zlmodzxzldeplem4  42860  zlmodzxzldep  42861  ldepsnlinclem1  42862  ldepsnlinclem2  42863  blennn0elnn  42939  nn0sumshdiglemA  42981  nn0sumshdiglemB  42982