Theorem eqeltri 2856

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  eqeltrri  2857  3eltr4i  2873  intab  4938  axrep6g  5245  unisn2  5269  inex2  5281  vpwex  5342  ord3ex  5352  zfpair  5386  vsnex  5400  snex  5404  opex  5439  opexOLD  5440  otex  5441  uniopel  5493  elvvuni  5732  isarep2  6622  fvex  6891  fvexi  6892  riotaex  7374  ovexi  7447  tpex  7747  oprabex  7973  oprabrexex2  7975  mpoexw  8077  mptmpoopabbrd  8080  tfrlem16  8382  1oex  8465  2oex  8467  1on  8468  2on  8469  3on  8472  4on  8473  oesuclem  8512  oecl  8524  o2p2e4  8528  nnecl  8601  1onnALT  8629  2onnALT  8631  3onn  8632  4onn  8633  mapsnf1o2  8901  sbthlem10  9094  cnvfi  9170  fnfi  9172  nnunifi  9261  pwfi  9288  prfiALT  9294  tpfi  9295  fczfsuppd  9356  cantnfvalf  9644  oemapwe  9673  cantnffval2  9674  cnfcom3clem  9684  ssttrcl  9694  r1fin  9755  scottex  9872  scottex2OLD  9885  hta  9901  htaOLD  9902  infxpenlem  10016  alephon  10072  alephfplem1  10107  dfac5lem4  10129  dfac5lem5  10130  kmlem10  10162  fin1a2lem10  10411  fin1a2lem12  10413  hsmexlem9  10427  axcc2lem  10438  domtriomlem  10444  axdc2lem  10450  axcclem  10459  brdom7disj  10534  brdom6disj  10535  iundom2g  10548  konigthlem  10577  canthwelem  10659  wunex2  10747  wunex3  10750  1nq  10937  1pr  11024  nrex1  11073  axcnex  11156  ax1cn  11158  pnfex  11286  mnfxr  11290  cju  12238  nnexALT  12259  2nn  12338  2re  12339  2cn  12340  3nn  12344  3re  12345  3cn  12346  4nn  12348  4re  12349  4cn  12350  5nn  12351  5re  12352  5cn  12353  6nn  12354  6re  12355  6cn  12356  7nn  12357  7re  12358  7cn  12359  8nn  12360  8re  12361  8cn  12362  9nn  12363  9re  12364  9cn  12365  nn0ex  12534  zexALT  12635  nneo  12705  zeo  12707  deccl  12751  10re  12759  decnncl  12760  numnncl2  12764  decnncl2  12765  numsucc  12781  numma2c  12787  numadd  12788  numaddc  12789  nummul1c  12790  nummul2c  12791  decmul1  12805  qexALT  13013  xrex  13037  xnegex  13260  xnegcl  13265  ixxssxr  13410  fz0to4untppr  13685  fz0to5un2tp  13686  om2uzuzi  14013  ltweuz  14025  axdc4uzlem  14047  seqex  14067  seqexw  14081  m1expcl2  14149  faccl  14347  facwordi  14353  faclbnd2  14355  bccl  14386  hashen1  14434  hashrabrsn  14436  hashunlei  14490  hashpw  14501  tpf1o  14566  s1cli  14672  ccat2s1p1  14697  cats1un  14790  revs1  14834  cshwsexa  14895  cats1cli  14928  cats1fvn  14929  crre  15201  remim  15204  climmpt  15658  sumex  15775  supcvg  15945  geo2lim  15964  prodex  15994  bpoly4  16145  ere  16175  eftlub  16197  efsep  16198  tan0  16239  ef01bndlem  16272  nn0o  16473  divalglem5  16487  divalglem9  16491  sadcf  16543  smupf  16568  crth  16869  phimullem  16870  pczpre  16939  pockthi  16999  prmreclem2  17009  igz  17026  0ramcl  17115  1259lem1  17223  1259lem2  17224  1259lem3  17225  1259lem4  17226  1259lem5  17227  1259prm  17228  2503lem1  17229  2503lem2  17230  2503lem3  17231  2503prm  17232  4001lem1  17233  4001lem2  17234  4001lem3  17235  4001lem4  17236  4001prm  17237  strle1  17250  ndxarg  17288  basendxnn  17311  plusgndxnn  17370  tsetndxnn  17439  plendxnn  17453  dsndxnn  17472  unifndxnn  17482  prdsbasex  17535  prdsds  17549  yonedalem3  18368  isposix  18412  chnub  18710  plusffval  18736  issubmgm2  18805  efmnd1hash  19001  efmnd2hash  19003  smndex1bas  19018  smndex1sgrp  19020  smndex1mnd  19022  smndex1id  19023  smndex2dbas  19026  smndex2hbas  19028  grpsubfval  19107  mulgfval  19192  symg1hash  19517  symg2hash  19519  symgvalstruct  19524  symgfisg  19595  psgnsn  19647  psgnprfval1  19649  odfval  19659  sylow2alem2  19745  efgsval2  19860  efgsp1  19864  pgpfaclem1  20210  dvdsrval  20502  isirred  20560  scaffval  21064  prmidl0  21541  cnfldex  21588  xrsex  21602  pzriprnglem4  21697  pzriprnglem5  21698  pzriprnglem6  21699  pzriprng1ALT  21709  znle  21749  znidomb  21774  cnmsgnsubg  21790  refld  21832  ipffval  21861  psrbag0  22278  psrbagsn  22279  psr1baslem  22410  mat1dimbas  22694  mat1dimscm  22697  mat1f1o  22700  mat1rhmelval  22702  m2detleib  22853  pmatcoe1fsupp  22926  indistopon  23226  iccordt  23439  conncompid  23656  ptbasfi  23807  ptcmpfi  24039  ustfn  24428  ust0  24446  ustn0  24447  tmslem  24708  nmfval  24814  cnbl0  24999  cnopn  25012  remet  25016  re2ndc  25027  zcld  25040  icccmp  25052  xrge0gsumle  25060  xrge0tsms  25061  xmetdcn  25065  divcn  25096  expcn  25100  iiconn  25115  idcncf  25146  cnmpopc  25156  cnrehmeo  25181  cnheiborlem  25182  rellycmp  25185  bndth  25186  evth2  25188  cnrlmod  25371  cnrlvec  25372  cncmet  25550  ishl2  25598  ehleudis  25646  ehleudisval  25647  finiunmbl  25772  ioombl1lem4  25789  vitalilem4  25839  vitalilem5  25840  ismbf2d  25868  mbfimaopnlem  25883  mbfi1fseqlem6  25948  itgex  25998  bddmulibl  26066  ditgex  26079  recnperf  26132  dvcnvrelem2  26245  ftc1  26269  mdegcl  26294  plyeq0lem  26436  iaa  26560  aaliou3lem4  26582  dvradcnv  26657  sincn  26680  coscn  26681  tanabsge  26744  circsubm  26790  reloggim  26836  logcn  26884  dvloglem  26885  logdmopn  26886  dvlog2  26890  2irrexpq  26968  cxpcn  26982  cxpcn3  26985  resqrtcn  26986  2logb9irrALT  27035  2irrexpqALT  27037  atanrecl  27148  atan1  27165  atansopn  27169  birthdaylem1  27188  birthday  27191  emcllem4  27235  emcllem6  27237  lgamgulmlem6  27270  basellem6  27322  ppiublem1  27438  bposlem6  27525  bposlem8  27527  lgslem4  27536  lgsdir2lem2  27562  selberglem1  27781  selberglem3  27783  selberg  27784  selbergs  27810  qdrng  27856  0no  28074  1no  28075  lrrecse  28207  precsexlem11  28482  seqsex  28550  nnsex  28583  n0bday  28617  n0subs  28628  n0p1nns  28636  dfnns2  28637  zsex  28645  bdayfinbndlem1  28732  z12sex  28739  z12shalf  28745  angmgmlem  29274  edgfndxnn  29449  structvtxvallem  29477  usgrexmpllem  29720  usgrexmpl  29723  uhgrspan1  29763  upgrres  29766  umgrres  29767  usgrres  29768  upgrres1  29773  umgrres1  29774  usgrres1  29775  fusgrfis  29790  cusgrres  29908  vtxdlfgrval  29945  vtxdusgr0edgnelALT  29956  umgr2v2e  29985  vtxdginducedm1lem1  29999  vtxdginducedm1fi  30004  finsumvtxdg2ssteplem4  30008  pthdlem1  30231  crctcshlem3  30287  2wlkd  30404  2wlkond  30405  2trlond  30407  2pthd  30408  2pthond  30410  umgr2adedgwlkonALT  30415  0pth  30595  wlk2v2e  30637  3wlkd  30650  3trlond  30653  3pthd  30654  3pthond  30655  3spthond  30657  eupthvdres  30715  eulerpathpr  30720  konigsbergumgr  30731  konigsberglem5  30736  konigsberg  30737  ex-lcm  30938  isvciOLD  31061  isnvi  31094  blocni  31286  hmoval  31291  cncph  31300  ipasslem7  31317  siilem2  31333  normlem2  31592  normlem3  31593  normlem6  31596  h0elch  31736  hhssabloilem  31742  hhsssh  31750  spansnji  32127  nonbooli  32132  3oalem5  32147  3oalem6  32148  3oai  32149  mayetes3i  32210  nmcexi  32507  nmbdfnlb  32531  rnelshi  32540  cnlnadjlem5  32552  pjbdlni  32630  golem2  32753  goeqi  32754  dp2clq  33326  rpdp2cl  33327  rpdp2cl2  33328  dpmul100  33342  rpdpcl  33348  xrge0tsmsd  33513  pmtrto1cl  33539  psgnfzto1stlem  33540  fzto1st  33543  psgnfzto1st  33545  nn0omnd  33784  xrge0slmod  33788  qusima  33837  fply1  33968  extvfvcl  34046  ply1degltdimlem  34132  ccfldextdgrr  34182  algextdeglem8  34234  constrfin  34256  2sqr3minply  34290  2sqr3nconstr  34291  cos9thpiminplylem4  34295  cos9thpiminplylem5  34296  cos9thpinconstrlem2  34300  circtopn  34347  circcn  34348  zarcmplem  34391  tpr2tp  34414  tpr2rico  34422  ordtprsval  34428  ordtprsuni  34429  ordtrestNEW  34431  ordtrest2NEWlem  34432  ordtrest2NEW  34433  ordtconnlem1  34434  mndpluscn  34436  xrge0pluscn  34450  xrge0mulc1cn  34451  xrge0haus  34454  lmlimxrge0  34458  lmxrge0  34462  qqhcn  34501  qqhucn  34502  esumex  34539  esumcst  34573  hasheuni  34595  esumcvg  34596  prsiga  34641  brsiga  34694  mbfmcnt  34779  sxbrsigalem3  34783  dya2iocuni  34794  dya2iocucvr  34795  sxbrsigalem1  34796  sxbrsiga  34801  eulerpartlemt  34882  fibp1  34912  coinflipprob  34991  coinfliprv  34994  ccatmulgnn0dir  35053  signswplusg  35063  hgt750lem2  35160  hgt750leme  35166  bnj105  35234  bnj918  35276  bnj95  35373  bnj852  35430  bnj865  35432  fineqvnttrclse  35650  subfacp1lem1  35758  subfacp1lem3  35761  subfacp1lem5  35763  subfacp1lem6  35764  kur14lem7  35791  iisconn  35831  iillysconn  35832  cvmliftlem5  35868  cvmliftlem8  35871  cvmliftlem10  35873  cvmlift2lem9  35890  satfv0  35937  goalrlem  35975  goalr  35976  satffunlem2lem2  35985  circum  36253  iexpire  36314  altopex  36540  colinearex  36640  ssoninhaus  37067  cnndvlem2  37235  bj-prex  37784  bj-prfromadj  37789  bj-pinftyccb  37973  taupi  38075  isbasisrelowl  38112  relowlpssretop  38118  poimirlem29  38398  poimirlem30  38399  poimirlem31  38400  dvasin  38453  dvacos  38454  areacirc  38462  upixp  38479  fdc  38495  lmclim2  38508  cncfres  38515  heibor1lem  38559  rrnval  38577  rrnmet  38579  reheibor  38589  isdrngo2  38708  isrngohom  38715  idlval  38763  isidl  38764  igenval  38811  scottexf  38916  cnvepresex  39084  preex  39240  renegclALT  39836  ldualfvadd  40001  cmtfvalN  40083  cvrfval  40141  cdleme31fv  41263  cdlemk40  41790  cdlemk56  41844  dibopelvalN  42016  dibopelval2  42018  dibelval3  42020  diblsmopel  42044  cdlemn11a  42080  dihopelvalcpre  42121  dihpN  42209  hlhilsca  42808  hlhilip  42821  3factsumint1  42887  lcmineqlem23  42917  aks4d1p1p6  42939  aks4d1p1p5  42941  aks6d1c6isolem2  43041  25or6to4  43072  itrere  43193  acos1half  43233  redvmptabs  43235  readvrec2  43236  sn-0tie0  43339  sn-itrere  43376  sn-retire  43377  prjspval  43449  flt4lem5e  43502  sn-isghm  43519  mapfzcons2  43564  jm2.23  43837  jm2.27dlem2  43851  jm2.27dlem4  43853  rmydioph  43855  rmxdioph  43857  expdiophlem2  43863  expdioph  43864  aomclem6  43900  pwslnmlem0  43932  frlmpwfi  43939  mncn0  43980  aaitgo  44003  arearect  44056  areaquad  44057  omcl3g  44175  comptiunov2i  44546  frege110  44813  frege133  44836  radcnvrat  45138  uzmptshftfval  45170  dvradcnv2  45171  binomcxplemdvbinom  45177  binomcxplemcvg  45178  binomcxplemnotnn0  45180  permaxinf2lem  45835  rfcnpre1  45853  fcnre  45859  refsumcn  45864  refsum2cnlem1  45871  unirnmapsn  46044  infxrpnf  46274  iocopn  46350  icoopn  46355  mccl  46428  clim1fr1  46431  islptre  46449  sumnnodd  46460  lptre2pt  46468  limclner  46479  limclr  46483  expfac  46485  0cnf  46705  icccncfext  46715  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  itgsin0pilem1  46778  iblempty  46793  itgvol0  46796  stoweidlem47  46875  stoweidlem53  46881  stoweidlem57  46885  stoweidlem59  46887  wallispilem3  46895  wallispilem4  46896  wallispilem5  46897  wallispi  46898  stirlinglem1  46902  stirlinglem8  46909  stirlinglem12  46913  stirlinglem13  46914  stirlinglem14  46915  stirlinglem15  46916  dirkerper  46924  dirkercncflem2  46932  fourierdlem16  46951  fourierdlem21  46956  fourierdlem22  46957  fourierdlem36  46971  fourierdlem42  46977  fourierdlem71  47005  fourierdlem83  47017  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  fourierdlem114  47048  sqwvfoura  47056  sqwvfourb  47057  fourierswlem  47058  fouriersw  47059  etransclem48  47110  salexct3  47170  salgencntex  47171  salgensscntex  47172  iooborel  47179  bor1sal  47183  gsumge0cl  47199  sge0tsms  47208  sge0isum  47255  nnfoctbdjlem  47283  isomenndlem  47358  mbfresmf  47567  incsmflem  47569  incsmf  47570  smfmbfcex  47588  decsmflem  47594  decsmf  47595  smflimlem1  47599  smfpimbor1lem2  47627  smf2id  47629  smfco  47630  smfpimcclem  47635  goldrarr  47746  lambert0  47755  tannpoly  47758  sprsymrelfolem1  48392  sprbisymrel  48399  fmtno0prm  48461  fmtno1prm  48462  fmtno2prm  48463  fmtno3prm  48465  fmtno4prm  48478  m2prm  48494  m3prm  48495  m5prm  48501  m7prm  48503  lighneallem4a  48511  nprmdvdsfacm1lem4  48526  0evenALTV  48604  1oddALTV  48606  2evenALTV  48608  6even  48627  7odd  48628  8even  48629  9gbo  48690  opstrgric  48842  ushggricedg  48843  grtri  48856  usgrexmpl1  48938  usgrexmpl1vtx  48939  usgrexmpl1edg  48940  usgrexmpl2  48943  usgrexmpl2vtx  48944  usgrexmpl2edg  48945  gpgprismgr4cycllem5  49015  pgnbgreunbgr  49041  pgn4cyclex  49042  uspgrex  49066  lmod1zrnlvec  49424  zlmodzxzldeplem1  49430  zlmodzxzldeplem3  49432  zlmodzxzldeplem4  49433  zlmodzxzldep  49434  ldepsnlinclem1  49435  ldepsnlinclem2  49436  blennn0elnn  49507  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550  itcovalpclem2  49601  itcovalt2lem2  49606  ackval42  49626  rrx2line  49670  rrx2linesl  49673  spheres  49676  2sphere  49679  2sphere0  49680  line2x  49684  line2y  49685  resipos  49901  functhinclem1  50370  prsthinc  50390  setc1oterm  50417  funcsetc1ocl  50422  funcsetc1o  50423  isinito2lem  50424  isinito3  50426  functermc2  50435  incat  50527  setc1onsubc  50528