MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqsstri Structured version   Unicode version

Theorem eqsstri 3374
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
Hypotheses
Ref Expression
eqsstr.1  |-  A  =  B
eqsstr.2  |-  B  C_  C
Assertion
Ref Expression
eqsstri  |-  A  C_  C

Proof of Theorem eqsstri
StepHypRef Expression
1 eqsstr.2 . 2  |-  B  C_  C
2 eqsstr.1 . . 3  |-  A  =  B
32sseq1i 3368 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 209 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  eqsstr3i  3375  ssrab2  3425  rabssab  3427  opabss  4341  brab2ga  4899  relopabi  4952  dmopabss  5038  resss  5122  relres  5126  rnin  5234  rnxpss  5258  cnvcnvss  5280  dmmptss  5322  fnres  5515  f0  5580  nfvres  5708  fvopab4ndm  5782  ffvresb  5861  funiunfv  5952  isoini2  6017  ovssunirn  6106  dmoprabss  6161  elmpt2cl  6293  omsson  6469  exse2  6506  fabexg  6522  frxp  6671  mpt2ndm0  6728  tposssxp  6738  dftpos4  6753  smores  6799  smores2  6801  iordsmo  6804  oawordeulem  6981  swoer  7117  swoord1  7118  swoord2  7119  ecss  7130  ecopovsym  7190  ecopovtrn  7191  ecopover  7192  sbthlem7  7415  nnfi  7491  imafi  7592  elfiun  7668  marypha1lem  7671  marypha2lem1  7673  ordtypelem2  7721  hartogslem1  7744  wemapso2OLD  7754  wemapso2lem  7755  wdomima2g  7789  inf3lem1  7822  wemapwe  7916  wemapweOLD  7917  tc2  7950  tz9.12lem1  7982  rankuni  8058  rankuniss  8061  rankmapu  8073  cplem1  8084  hta  8092  r0weon  8167  infxpenlem  8168  ackbij1lem9  8385  ackbij1lem10  8386  ackbij1b  8396  cofsmo  8426  sdom2en01  8459  fin23lem26  8482  fin23lem28  8497  fin23lem30  8499  isf32lem5  8514  isf32lem6  8515  isf32lem7  8516  isf32lem8  8517  fin56  8550  fin1a2lem9  8565  hsmexlem4  8586  hsmexlem5  8587  hsmexlem6  8588  axdc3lem  8607  axdc3lem2  8608  axcclem  8614  zorn2lem1  8653  zorn2lem3  8655  zorn2lem4  8656  zorn2lem5  8657  imadomg  8689  iundom2g  8692  smobeth  8738  canth4  8801  gruina  8972  grur1a  8973  pinn  9034  niex  9037  ltsopi  9044  ltrelpi  9045  dmaddpi  9046  dmmulpi  9047  enqex  9078  0nnq  9080  elpqn  9081  ltrelnq  9082  nqerf  9086  nqerrel  9088  dmrecnq  9124  lterpq  9126  ltrelpr  9154  enrex  9224  ltrelsr  9225  dmaddsr  9239  dmmulsr  9240  ltrelre  9288  axaddf  9299  axmulf  9300  ltrelxr  9425  lerelxr  9427  nn0ssre  10570  nn0ssz  10654  uzsupss  10934  rpnnen1lem1  10966  rpnnen1lem2  10967  rpnnen1lem3  10968  rpnnen1lem5  10970  rpre  10984  uzsup  11685  fzfi  11777  swrd00  12297  sqrlem3  12717  sqrlem5  12719  cau3  12826  caubnd  12829  limsupgre  12942  rlimpm  12961  rlimclim  13007  isercolllem1  13125  isercolllem2  13126  isercoll  13128  caurcvg  13137  caucvg  13139  iseraltlem2  13143  iseraltlem3  13144  zsum  13178  fsumcvg3  13189  climfsum  13265  ackbijnn  13273  infcvgaux1i  13301  dvdszrcl  13522  divalglem2  13581  divalglem5  13583  divalglem8  13586  gcdcllem3  13679  bezoutlem2  13705  bezoutlem3  13706  maxprmfct  13781  phimullem  13836  eulerthlem2  13839  prmdiveq  13843  prmdivdiv  13844  pclem  13887  infpn2  13956  prmreclem2  13960  prmreclem3  13961  prmreclem5  13963  4sqlem1  13991  4sqlem13  14000  4sqlem14  14001  4sqlem17  14004  4sqlem18  14005  4sqlem19  14006  vdwnnlem3  14040  ramcl2lem  14052  ramtcl  14053  ramtcl2  14054  ramtub  14055  ramub1lem2  14070  structcnvcnv  14167  fvsetsid  14181  strlemor0  14246  strlemor1  14247  strleun  14250  imasdsval2  14436  gsumval1  15488  nmzsubg  15701  nmznsg  15704  conjnmz  15759  conjnmzb  15760  gicer  15783  gastacl  15806  symgbasfi  15870  mvdco  15930  symgsssg  15952  sylow1lem2  16077  sylow1lem3  16078  sylow1lem4  16079  sylow1lem5  16080  sylow2a  16097  sylow3lem2  16106  efglem  16192  efgtf  16198  efgtlen  16202  efginvrel2  16203  efginvrel1  16204  efgsfo  16215  efgredlemg  16218  efgredleme  16219  efgredlemd  16220  efgredlemc  16221  efgredlem  16223  efgred  16224  efgrelexlemb  16226  efgcpbllemb  16231  frgpinv  16240  frgpuplem  16248  frgpupf  16249  frgpup1  16251  frgpnabllem2  16331  gsumval3OLD  16361  gsumval3lem1  16362  gsumval3lem2  16363  gsumval3  16364  ablfacrplem  16539  ablfacrp2  16541  ablfac1eu  16547  pgpfaclem1  16555  ablfaclem2  16560  ablfaclem3  16561  lspsolvlem  17144  lbsextlem2  17161  lbsextlem3  17162  lbsextlem4  17163  rrgeq0  17282  rrgss  17285  psrbagconf1o  17377  psrass1lem  17380  mplbasss  17441  ply1bascl  17557  coe1mul2lem2  17619  znf1o  17825  zntoslem  17830  cygznlem2a  17841  psgnghm  17851  pjpm  17974  dsmmbase  18001  frlmsslsp  18064  frlmsslspOLD  18065  mretopd  18537  ordtbas  18637  leordtval2  18657  lecldbas  18664  lmfval  18677  lmbrf  18705  cnconst2  18728  hauscmplem  18850  concompcld  18879  hauspwdom  18946  txuni2  18979  xkouni  19013  xkoccn  19033  txkgen  19066  qtoptop2  19113  kqdisj  19146  hmphtop  19192  hmpher  19198  uzrest  19311  uzfbas  19312  lmflf  19419  ptcmplem1  19465  ptcmplem3  19467  tgpconcompeqg  19523  tgpconcomp  19524  ustn0  19636  imasdsf1olem  19789  xmeter  19849  blcld  19921  isngp2  20030  xrtgioo  20224  iccntr  20239  icccmplem1  20240  icccmplem2  20241  icccmplem3  20242  xmetdcn  20256  metdcn  20258  metdscn2  20274  icchmeo  20354  cnheiborlem  20367  lmmbrf  20614  iscau4  20631  iscauf  20632  caucfil  20635  lmclimf  20655  rrxf  20741  ivthlem1  20776  ivthlem2  20777  ivthlem3  20778  ovolsslem  20808  ovolicc2lem3  20843  ovolicc2lem4  20844  ovolicc2lem5  20845  ovolicc2  20846  volf  20853  uniioombllem3  20906  uniioombllem4  20907  uniioombllem5  20908  dyadmbllem  20920  dyadmbl  20921  volcn  20927  mbfimaopnlem  20974  mbflimsup  20985  i1f1  21009  itg2lcl  21046  iblmbf  21086  itgioo  21134  itgsplitioo  21156  limcflflem  21196  limcflf  21197  limcresi  21201  lhop  21329  dvfsumlem1  21339  dvfsumlem2  21340  dvfsumlem3  21341  dvfsumlem4  21342  dvfsumrlimge0  21343  dvfsumrlim  21344  dvfsumrlim2  21345  dvfsum2  21347  vieta1lem1  21660  vieta1lem2  21661  psercnlem2  21773  psercnlem1  21774  psercn  21775  pserdvlem1  21776  pserdvlem2  21777  pserdv  21778  pserdv2  21779  abelthlem4  21783  abelthlem6  21785  abelthlem9  21789  abelth  21790  logcnlem5  21975  dvlog  21980  dvlog2lem  21981  dvlog2  21982  cxpcn3lem  22069  cxpcn3  22070  sqrcn  22072  1cubr  22121  atansssdm  22212  atancn  22215  jensen  22266  wilthlem1  22290  ftalem3  22296  dvdsflip  22406  musum  22415  dvdsmulf1o  22418  fsumdvdsmul  22419  ppiub  22427  lgsfcl2  22525  lgsquadlem1  22577  lgsquadlem2  22578  lgsquadlem3  22579  2sqlem7  22593  rpvmasum2  22645  dchrisum0re  22646  dchrisum0lema  22647  dchrisum0lem1b  22648  dchrisum0lem1  22649  dchrisum0lem2a  22650  dchrisum0lem2  22651  dchrisum0lem3  22652  dchrisum0  22653  pntlem3  22742  axtgcgrrflx  22807  axtgcgrid  22808  axtgsegcon  22809  axtg5seg  22810  axtgbtwnid  22811  axtgpasch  22812  axtgcont1  22813  tglng  22860  axcontlem2  23033  axcontlem7  23038  axcontlem8  23039  axcontlem10  23041  nbgraf1olem1  23172  issubgoi  23619  flddivrng  23724  phnv  24036  htthlem  24141  hlimadd  24417  hlimcaui  24461  hhsscms  24502  occllem  24528  shjshsi  24717  3oalem4  24890  pjfi  24929  dmadjss  25113  nlelshi  25286  nlelchi  25287  hmopidmchi  25377  atssch  25569  shatomistici  25587  mptctf  25844  fcobijfs  25849  cnre2csqima  26194  raddcn  26212  rrhre  26300  esumsn  26368  sxbrsiga  26558  oddpwdc  26584  eulerpartlem1  26597  eulerpartlemt  26601  eulerpartgbij  26602  eulerpartlemmf  26605  eulerpartlemgvv  26606  eulerpartlemgh  26608  sseqf  26622  ballotlemoex  26715  ballotlemfmpn  26724  ballotth  26767  signswch  26809  lgamucov  26871  lgamucov2  26872  subfacp1lem3  26917  subfacp1lem5  26919  erdszelem2  26927  kur14lem3  26943  kur14lem6  26946  kur14lem7  26947  kur14lem9  26949  cvmlift2lem12  27050  ghomgrpilem2  27151  divcnvshft  27244  clim2prod  27249  ntrivcvg  27258  ntrivcvgfvn0  27260  ntrivcvgtail  27261  ntrivcvgmullem  27262  ntrivcvgmul  27263  zprod  27296  dfpo2  27411  predss  27478  wfrlem7  27576  wlimss  27612  frrlem7  27624  txpss3v  27755  pprodss4v  27761  relsset  27765  fixssdm  27783  fixssrn  27784  limitssson  27788  funpartss  27821  colinearex  27937  dvcncxp1  28318  dvcnsqr  28319  dvasin  28321  dvacos  28322  areacirc  28330  fneer  28401  neibastop1  28421  neibastop2lem  28422  filnetlem2  28441  filnetlem3  28442  caures  28497  bnd2lem  28531  ismtyres  28548  eldiophb  28937  monotuz  29124  fglmod  29268  pwssplit4  29284  pwfi2f1o  29293  arearect  29433  rabexgf  29588  stoweidlem26  29664  stoweidlem44  29682  stoweidlem50  29688  stoweidlem51  29689  stoweidlem52  29690  stoweidlem57  29695  stoweidlem59  29697  disjxwwlkn  30407  clwlknclwlkdifnum  30422  frgrawopreg1  30486  frgrawopreg2  30487  bnj21  31405  bnj1146  31484  bnj1292  31508  bnj1293  31509  bnj1145  31683  bnj1177  31696  bj-tagss  32053  bj-vecmod  32149  bj-abelcmnd  32152  bj-rrvecvec  32159  toycom  32188  dihglblem2N  34509  lcdvbase  34808  mapdunirnN  34865
  Copyright terms: Public domain W3C validator