Theorem eqeltri 2909

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

Syntax hints:   = wceq 1533   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893

This theorem is referenced by:  eqeltrri  2910  3eltr4i  2926  intab  4898  unisn2  5208  inex2  5214  vpwex  5270  ord3ex  5279  zfpair  5313  opex  5348  otex  5349  uniopel  5398  elvvuni  5622  predasetex  6157  isarep2  6437  fvex  6677  fvexi  6678  riotaex  7112  ovexi  7184  tpex  7464  oprabex  7671  oprabrexex2  7673  mpoexw  7770  tfrlem16  8023  1on  8103  2on  8105  2oex  8106  3on  8108  4on  8109  oesuclem  8144  oecl  8156  o2p2e4  8160  nnecl  8233  1onn  8259  2onn  8260  3onn  8261  4onn  8262  mapsnf1o2  8452  sbthlem10  8630  nnunifi  8763  xpfi  8783  prfi  8787  tpfi  8788  fnfi  8790  pwfi  8813  fczfsuppd  8845  inf0  9078  cantnfvalf  9122  oemapwe  9151  cantnffval2  9152  cnfcom3clem  9162  r1fin  9196  hta  9320  infxpenlem  9433  alephon  9489  alephfplem1  9524  dfac5lem4  9546  dfac5lem5  9547  kmlem10  9579  fin1a2lem10  9825  fin1a2lem12  9827  hsmexlem9  9841  axcc2lem  9852  domtriomlem  9858  axdc2lem  9864  axcclem  9873  brdom7disj  9947  brdom6disj  9948  iundom2g  9956  konigthlem  9984  canthwelem  10066  wunex2  10154  wunex3  10157  1nq  10344  1pr  10431  nrex1  10480  axcnex  10563  ax1cn  10565  pnfex  10688  mnfxr  10692  inelr  11622  cju  11628  nnexALT  11634  2nn  11704  2re  11705  2cn  11706  3nn  11710  3re  11711  3cn  11712  4nn  11714  4re  11715  4cn  11716  5nn  11717  5re  11718  5cn  11719  6nn  11720  6re  11721  6cn  11722  7nn  11723  7re  11724  7cn  11725  8nn  11726  8re  11727  8cn  11728  9nn  11729  9re  11730  9cn  11731  nn0ex  11897  zexALT  11995  nneo  12060  zeo  12062  deccl  12107  10re  12111  decnncl  12112  numnncl2  12115  decnncl2  12116  numsucc  12132  numma2c  12138  numadd  12139  numaddc  12140  nummul1c  12141  nummul2c  12142  decmul1  12156  qexALT  12357  xrex  12380  xnegex  12595  xnegcl  12600  ixxssxr  12744  om2uzuzi  13311  ltweuz  13323  axdc4uzlem  13345  seqex  13365  seqexw  13379  m1expcl2  13445  faccl  13637  facwordi  13643  faclbnd2  13645  bccl  13676  hashen1  13725  hashrabrsn  13727  hashunlei  13780  hashpw  13791  s1cli  13953  ccat2s1p1  13979  cats1un  14077  revs1  14121  cshwsexa  14180  cats1cli  14213  cats1fvn  14214  crre  14467  remim  14470  climmpt  14922  sumex  15038  supcvg  15205  geo2lim  15225  prodex  15255  bpoly4  15407  ere  15436  eftlub  15456  efsep  15457  tan0  15498  ef01bndlem  15531  nn0o  15728  divalglem5  15742  divalglem9  15746  sadcf  15796  smupf  15821  crth  16109  phimullem  16110  pczpre  16178  pockthi  16237  prmreclem2  16247  igz  16264  0ramcl  16353  1259lem1  16458  1259lem2  16459  1259lem3  16460  1259lem4  16461  1259lem5  16462  1259prm  16463  2503lem1  16464  2503lem2  16465  2503lem3  16466  2503prm  16467  4001lem1  16468  4001lem2  16469  4001lem3  16470  4001lem4  16471  4001prm  16472  ndxarg  16502  basendxnn  16542  strle1  16586  prdsbasex  16718  prdsds  16731  yonedalem3  17524  isposix  17561  plusffval  17852  efmnd1hash  18051  efmnd2hash  18053  smndex1bas  18065  smndex1sgrp  18067  smndex1mnd  18069  smndex1id  18070  smndex2dbas  18073  smndex2hbas  18075  grpsubfval  18141  mulgfval  18220  symg1hash  18512  symg2hash  18514  symgvalstruct  18519  symgfisg  18590  psgnsn  18642  psgnprfval1  18644  odfval  18654  sylow2alem2  18737  efgsval2  18853  efgsp1  18857  pgpfaclem1  19197  dvdsrval  19389  isirred  19443  scaffval  19646  psrbag0  20268  psrbagsn  20269  psr1baslem  20347  xrsex  20554  zlmlem  20658  znle  20677  znidomb  20702  cnmsgnsubg  20715  refld  20757  ipffval  20786  mat1dimbas  21075  mat1dimscm  21078  mat1f1o  21081  mat1rhmelval  21083  m2detleib  21234  pmatcoe1fsupp  21303  indistopon  21603  iccordt  21816  conncompid  22033  ptbasfi  22183  ptcmpfi  22415  ustfn  22804  ust0  22822  ustn0  22823  tmslem  23086  nmfval  23192  tnglem  23243  cnbl0  23376  cnopn  23389  remet  23392  re2ndc  23403  zcld  23415  icccmp  23427  xrge0gsumle  23435  xrge0tsms  23436  xmetdcn  23440  divcn  23470  expcn  23474  iiconn  23489  cnmpopc  23526  cnrehmeo  23551  cnheiborlem  23552  rellycmp  23555  bndth  23556  evth2  23558  cnrlmod  23741  cnrlvec  23742  cncmet  23919  ishl2  23967  ehleudis  24015  ehleudisval  24016  finiunmbl  24139  ioombl1lem4  24156  vitalilem4  24206  vitalilem5  24207  ismbf2d  24235  mbfimaopnlem  24250  mbfi1fseqlem6  24315  itgex  24365  bddmulibl  24433  ditgex  24444  recnperf  24497  dvcnvrelem2  24609  ftc1  24633  mdegcl  24657  plyeq0lem  24794  aaliou3lem4  24929  dvradcnv  25003  sincn  25026  coscn  25027  tanabsge  25086  circsubm  25131  reloggim  25176  logcn  25224  dvloglem  25225  logdmopn  25226  dvlog2  25230  2irrexpq  25307  cxpcn  25320  cxpcn3  25323  resqrtcn  25324  2logb9irrALT  25370  2irrexpqALT  25372  atanrecl  25483  atan1  25500  atansopn  25504  birthdaylem1  25523  birthday  25526  emcllem4  25570  emcllem6  25572  lgamgulmlem6  25605  basellem6  25657  ppiublem1  25772  bposlem6  25859  bposlem8  25861  lgslem4  25870  lgsdir2lem2  25896  selberglem1  26115  selberglem3  26117  selberg  26118  selbergs  26144  qdrng  26190  edgfndxnn  26771  structvtxvallem  26799  usgrexmpllem  27036  usgrexmpl  27039  uhgrspan1  27079  upgrres  27082  umgrres  27083  usgrres  27084  upgrres1  27089  umgrres1  27090  usgrres1  27091  fusgrfis  27106  cusgrres  27224  vtxdlfgrval  27261  vtxdusgr0edgnelALT  27272  umgr2v2e  27301  vtxdginducedm1lem1  27315  vtxdginducedm1fi  27320  finsumvtxdg2ssteplem4  27324  pthdlem1  27541  crctcshlem3  27591  2wlkd  27709  2wlkond  27710  2trlond  27712  2pthd  27713  2pthond  27715  umgr2adedgwlkonALT  27720  0pth  27898  wlk2v2e  27930  3wlkd  27943  3trlond  27946  3pthd  27947  3pthond  27948  3spthond  27950  eupthvdres  28008  eulerpathpr  28013  konigsbergumgr  28024  konigsberglem5  28029  konigsberg  28030  ex-lcm  28231  isvciOLD  28351  isnvi  28384  blocni  28576  hmoval  28581  cncph  28590  ipasslem7  28607  siilem2  28623  normlem2  28882  normlem3  28883  normlem6  28886  h0elch  29026  hhssabloilem  29032  hhsssh  29040  spansnji  29417  nonbooli  29422  3oalem5  29437  3oalem6  29438  3oai  29439  mayetes3i  29500  nmcexi  29797  nmbdfnlb  29821  rnelshi  29830  cnlnadjlem5  29842  pjbdlni  29920  golem2  30043  goeqi  30044  dp2clq  30552  rpdp2cl  30553  rpdp2cl2  30554  dpmul100  30568  rpdpcl  30574  xrge0tsmsd  30687  pmtrto1cl  30736  psgnfzto1stlem  30737  fzto1st  30740  psgnfzto1st  30742  nn0omnd  30909  xrge0slmod  30912  fply1  30926  ccfldextdgrr  31052  circtopn  31096  circcn  31097  tpr2tp  31142  tpr2rico  31150  ordtprsval  31156  ordtprsuni  31157  ordtrestNEW  31159  ordtrest2NEWlem  31160  ordtrest2NEW  31161  ordtconnlem1  31162  mndpluscn  31164  xrge0pluscn  31178  xrge0mulc1cn  31179  xrge0haus  31182  lmlimxrge0  31186  lmxrge0  31190  qqhcn  31227  qqhucn  31228  esumex  31283  esumcst  31317  hasheuni  31339  esumcvg  31340  prsiga  31385  brsiga  31437  mbfmcnt  31521  sxbrsigalem3  31525  dya2iocuni  31536  dya2iocucvr  31537  sxbrsigalem1  31538  sxbrsiga  31543  eulerpartlemt  31624  fibp1  31654  coinflipprob  31732  coinfliprv  31735  ccatmulgnn0dir  31807  signswplusg  31820  hgt750lem2  31918  hgt750leme  31924  bnj105  31989  bnj918  32032  bnj95  32131  bnj852  32188  bnj865  32190  subfacp1lem1  32421  subfacp1lem3  32424  subfacp1lem5  32426  subfacp1lem6  32427  kur14lem7  32454  iisconn  32494  iillysconn  32495  cvmliftlem5  32531  cvmliftlem8  32534  cvmliftlem10  32536  cvmlift2lem9  32553  satfv0  32600  goalrlem  32638  goalr  32639  satffunlem2lem2  32648  circum  32912  iexpire  32962  trpredex  33071  altopex  33416  colinearex  33516  ssoninhaus  33791  cnndvlem2  33872  bj-pinftyccb  34497  taupi  34598  isbasisrelowl  34633  relowlpssretop  34639  poimirlem29  34915  poimirlem30  34916  poimirlem31  34917  dvasin  34972  dvacos  34973  areacirc  34981  upixp  34998  fdc  35014  lmclim2  35027  idcncf  35032  cncfres  35037  heibor1lem  35081  rrnval  35099  rrnmet  35101  reheibor  35111  isdrngo2  35230  isrngohom  35237  idlval  35285  isidl  35286  igenval  35333  scottexf  35440  cnvepresex  35585  renegclALT  36093  ldualfvadd  36258  cmtfvalN  36340  cvrfval  36398  cdleme31fv  37520  cdlemk40  38047  cdlemk56  38101  dibopelvalN  38273  dibopelval2  38275  dibelval3  38277  diblsmopel  38301  cdlemn11a  38337  dihopelvalcpre  38378  dihpN  38466  hlhilsca  39065  hlhilip  39078  prjspval  39246  mapfzcons2  39309  jm2.23  39586  jm2.27dlem2  39600  jm2.27dlem4  39602  rmydioph  39604  rmxdioph  39606  expdiophlem2  39612  expdioph  39613  aomclem6  39652  pwslnmlem0  39684  frlmpwfi  39691  mncn0  39732  aaitgo  39755  arearect  39815  areaquad  39816  comptiunov2i  40044  frege110  40312  frege133  40335  scottex2  40574  radcnvrat  40639  uzmptshftfval  40671  dvradcnv2  40672  binomcxplemdvbinom  40678  binomcxplemcvg  40679  binomcxplemnotnn0  40681  rfcnpre1  41269  fcnre  41275  refsumcn  41280  refsum2cnlem1  41287  unirnmapsn  41470  infxrpnf  41714  iocopn  41789  icoopn  41794  mccl  41872  clim1fr1  41875  islptre  41893  sumnnodd  41904  lptre2pt  41914  limclner  41925  limclr  41929  expfac  41931  0cnf  42153  icccncfext  42163  ioodvbdlimc1lem2  42210  ioodvbdlimc2lem  42212  itgsin0pilem1  42228  iblempty  42243  itgvol0  42246  stoweidlem47  42326  stoweidlem53  42332  stoweidlem57  42336  stoweidlem59  42338  wallispilem3  42346  wallispilem4  42347  wallispilem5  42348  wallispi  42349  stirlinglem1  42353  stirlinglem8  42360  stirlinglem12  42364  stirlinglem13  42365  stirlinglem14  42366  stirlinglem15  42367  dirkerper  42375  dirkercncflem2  42383  fourierdlem16  42402  fourierdlem21  42407  fourierdlem22  42408  fourierdlem36  42422  fourierdlem42  42428  fourierdlem71  42456  fourierdlem83  42468  fourierdlem102  42487  fourierdlem103  42488  fourierdlem104  42489  fourierdlem111  42496  fourierdlem112  42497  fourierdlem114  42499  sqwvfoura  42507  sqwvfourb  42508  fourierswlem  42509  fouriersw  42510  etransclem48  42561  salexct3  42619  salgencntex  42620  salgensscntex  42621  iooborel  42628  bor1sal  42632  gsumge0cl  42647  sge0tsms  42656  sge0isum  42703  nnfoctbdjlem  42731  isomenndlem  42806  mbfresmf  43010  incsmflem  43012  incsmf  43013  smfmbfcex  43030  decsmflem  43036  decsmf  43037  smflimlem1  43041  smfpimbor1lem2  43068  smf2id  43070  smfco  43071  smfpimcclem  43075  sprsymrelfolem1  43648  sprbisymrel  43655  fmtno0prm  43714  fmtno1prm  43715  fmtno2prm  43716  fmtno3prm  43718  fmtno4prm  43731  m2prm  43747  m3prm  43748  m5prm  43755  m7prm  43758  lighneallem4a  43767  0evenALTV  43847  1oddALTV  43849  2evenALTV  43851  6even  43870  7odd  43871  8even  43872  9gbo  43933  strisomgrop  43999  ushrisomgr  44000  uspgrex  44019  issubmgm2  44051  lmod1zrnlvec  44543  zlmodzxzldeplem1  44549  zlmodzxzldeplem3  44551  zlmodzxzldeplem4  44552  zlmodzxzldep  44553  ldepsnlinclem1  44554  ldepsnlinclem2  44555  blennn0elnn  44631  nn0sumshdiglemA  44673  nn0sumshdiglemB  44674  rrx2line  44721  rrx2linesl  44724  spheres  44727  2sphere  44730  2sphere0  44731  line2x  44735  line2y  44736