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

Theorem sseq1 3233
Description: Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sseq1  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )

Proof of Theorem sseq1
StepHypRef Expression
1 eqss 3228 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
2 sstr2 3220 . . . 4  |-  ( B 
C_  A  ->  ( A  C_  C  ->  B  C_  C ) )
32adantl 452 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  ->  B  C_  C )
)
4 sstr2 3220 . . . 4  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
54adantr 451 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( B  C_  C  ->  A  C_  C )
)
63, 5impbid 183 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  <->  B 
C_  C ) )
71, 6sylbi 187 1  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1633    C_ wss 3186
This theorem is referenced by:  sseq12  3235  sseq1i  3236  sseq1d  3239  nssne2  3269  psseq1  3297  uneqdifeq  3576  sbss  3597  pwjust  3660  elpw  3665  elpwg  3666  pwpw0  3800  sssn  3809  ssunsn2  3810  pwsnALT  3859  unimax  3898  trss  4159  elssabg  4203  intabs  4209  nnullss  4272  exss  4273  fri  4392  onssmin  4625  tfis  4682  tfisi  4686  releq  4808  xpsspw  4834  iss  5035  relcnvtr  5229  fununi  5353  funcnvuni  5354  ffoss  5543  ssimaex  5622  isofrlem  5879  f1oweALT  5893  frxp  6267  tfrlem1  6433  oawordeu  6595  qsss  6762  boxcutc  6902  sbthlem2  7015  sbth  7024  php  7088  isinf  7119  unbnn2  7159  domunfican  7174  fiint  7178  finsschain  7207  indexfi  7208  dffi3  7229  hartogslem1  7302  sucprcreg  7358  cantnfval2  7415  cantnfle  7417  cantnflem1  7436  tz9.1  7456  setind  7464  tcvalg  7468  scott0  7601  bnd2  7608  carduni  7659  cardaleph  7761  alephinit  7767  aceq3lem  7792  dfac12lem3  7816  infmap2  7889  cflem  7917  cflm  7921  cflecard  7924  cfeq0  7927  cfsuc  7928  cfflb  7930  cfslb  7937  cfslb2n  7939  coftr  7944  fin23lem13  8003  fin23lem16  8006  fin23lem19  8007  fin23lem29  8012  fin1a2lem13  8083  itunitc  8092  domtriomlem  8113  axdc3lem2  8122  zorn2lem7  8174  zornn0g  8177  fpwwe2lem5  8301  pwfseqlem4a  8328  pwfseqlem4  8329  wunfi  8388  wunex2  8405  wuncval  8409  rankcf  8444  tskuni  8450  axgroth6  8495  axgroth3  8498  axgroth4  8499  fzoss1  10943  hashf1lem2  11441  sumeq1f  12208  fsumcvg3  12249  fsum2d  12281  fsumabs  12306  fsumrlim  12316  fsumo1  12317  fsumiun  12326  vdwmc  13072  restsspw  13385  ismred2  13554  mrcval  13561  mrcuni  13572  acsfn  13610  isssc  13746  drsdirfi  14121  clatlem  14265  clatl  14269  ipodrsima  14317  cntzssv  14853  isslw  14968  sylow2alem2  14978  sylow2a  14979  efgval  15075  gsumzaddlem  15252  ablfac1eulem  15356  lspval  15781  lspindpi  15934  aspval  16117  mplsubglem  16228  mpllsslem  16229  mplcoe1  16258  mplcoe2  16260  znf1o  16561  zntoslem  16566  uniopn  16699  fiinopn  16703  fiinbas  16746  baspartn  16748  eltg2  16752  eltg3  16756  topbas  16766  pptbas  16801  clsval  16830  neival  16895  neiint  16897  neips  16906  opnneissb  16907  opnssneib  16908  innei  16918  restbas  16945  restcld  16959  restcls  16967  restntr  16968  cnpdis  17077  nrmsep3  17139  cmpsublem  17182  cmpsub  17183  fiuncmp  17187  uncon  17211  1stcfb  17227  2ndc1stc  17233  1stcrest  17235  2ndcctbss  17237  2ndcomap  17240  dis2ndc  17242  lly1stc  17278  llycmpkgen2  17301  txbas  17318  eltx  17319  ptuni2  17327  ptpjopn  17362  ptcld  17363  txlm  17398  tx1stc  17400  txkgen  17402  xkopt  17405  xkococnlem  17409  ptcmpfi  17560  fbssfi  17584  opnfbas  17589  isfil2  17603  isfildlem  17604  snfil  17611  fsubbas  17614  ssfg  17619  fgss2  17621  fgcl  17625  fbasrn  17631  fgtr  17637  ufli  17661  uffix  17668  rnelfmlem  17699  fclscf  17772  alexsublem  17790  alexsubALTlem2  17794  alexsubALTlem3  17795  alexsubALTlem4  17796  alexsubALT  17797  tmdgsum2  17831  subgntr  17841  opnsubg  17842  divstgpopn  17854  tsmsfbas  17862  tsmsgsum  17873  tsmsres  17878  tsmsf1o  17879  tsmsxplem1  17887  tsmsxp  17889  blssex  18025  neibl  18099  blcld  18103  met1stc  18119  met2ndci  18120  metrest  18122  prdsxmslem2  18127  dscopn  18148  isngp2  18171  tgioo  18354  tgqioo  18358  zdis  18374  xrge0tsms  18391  fsumcn  18426  ovolval  18886  volivth  19015  vitalilem2  19017  itgfsum  19234  limcun  19298  recnprss  19307  dvmptfsum  19375  ftc1a  19437  plyssc  19635  efopn  20058  jensen  20336  hhsssh  21901  shintcl  21964  chintcl  21966  spanval  21967  omlsi  22038  pjoml  22070  chnlen0  22078  chsscon3  22134  chlejb1  22146  chnle  22148  spanun  22179  h1datom  22216  cmbr4i  22235  pjoml2  22245  pjoml3  22246  lecm  22251  osumcor2i  22278  osum  22279  spansncv  22287  pjcjt2  22326  pjopyth  22354  pjss1coi  22798  hstel2  22854  stj  22870  stcltr1i  22909  mdi  22930  mdbr3  22932  mdbr4  22933  dmdbr  22934  dmdmd  22935  dmdbr5  22943  mdsl1i  22956  mdslmd1lem3  22962  mdslmd1lem4  22963  mdslmd1i  22964  csmdsymi  22969  atss  22981  atom1d  22988  superpos  22989  chcv1  22990  shatomici  22993  shatomistici  22996  hatomistici  22997  chrelat2  23005  chirredi  23029  atcvat4i  23032  mdsymlem2  23039  mdsymlem6  23043  dmdbr6ati  23058  dmdbr7ati  23059  xrge0tsmsd  23360  tpr2rico  23379  isust  23420  ustssel  23422  ustincl  23424  ustdiag  23425  ustinvel  23426  ustexhalf  23427  ust0  23432  restutop  23448  metustfbas  23499  cfilucfil  23501  metustbl  23508  restmetu  23513  issiga  23670  isrnsigaOLD  23671  isrnsiga  23672  sigagenval  23699  measiuns  23745  dya2icoseg  23801  dya2iocnrect  23805  dya2iocuni  23807  kur14lem1  24021  cvmopnlem  24093  rtrclreclem.min  24328  prodeq1f  24411  dfon2lem3  24526  dfon2lem7  24530  frmin  24627  wfrlem1  24641  wfrlem4  24644  wfrlem15  24655  frrlem1  24666  frrlem3  24668  brsset  24814  bpolyval  25170  onsucsuccmpi  25268  ovoliunnfl  25315  refssex  25430  fness  25431  fneref  25433  fnessref  25442  neibastop2lem  25458  topmeet  25462  fnejoin2  25467  tailfb  25475  filnetlem4  25479  indexa  25561  indexdom  25562  neificl  25616  istotbnd3  25643  sstotbnd2  25646  sstotbnd  25647  equivtotbnd  25650  ssbnd  25660  heiborlem1  25683  heiborlem6  25688  heiborlem8  25690  heiborlem10  25692  unichnidl  25804  pridl  25810  ismaxidl  25813  igenval  25834  igenval2  25839  ispridlc  25843  ismrcd1  25921  ismrcd2  25922  ismrc  25924  mzpcompact2lem  25977  aomclem6  26304  hbtlem6  26481  rgspnval  26521  pmtrfrn  26548  stoweidlem34  26931  stoweidlem51  26948  stoweidlem52  26949  prelpw  27229  usgraedgprv  27348  frisusgranb  27589  onfrALTlem5  27801  onfrALTlem5VD  28172  bnj1143  28333  bnj517  28428  bnj1118  28525  bnj1145  28534  bnj1154  28540  bnj1452  28593  bnj1498  28602  lsmsat  29016  lssatomic  29019  lssats  29020  lsat0cv  29041  lcvexchlem4  29045  lcvexchlem5  29046  lsatcvatlem  29057  l1cvpat  29062  ispsubsp  29752  linepsubN  29759  pclvalN  29897  ispsubclN  29944  ispsubcl2N  29954  pclfinclN  29957  diaelrnN  31053  docavalN  31131  dochval  31359  dvh4dimat  31446  dochexmidlem1  31468  lpolconN  31495  mapdordlem2  31645
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-in 3193  df-ss 3200
  Copyright terms: Public domain W3C validator