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

Theorem sseq1 3199
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 3194 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
2 sstr2 3186 . . . 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 3186 . . . 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 1623    C_ wss 3152
This theorem is referenced by:  sseq12  3201  sseq1i  3202  sseq1d  3205  nssne2  3235  psseq1  3263  uneqdifeq  3542  sbss  3563  pwjust  3626  elpw  3631  elpwg  3632  pwpw0  3763  sssn  3772  ssunsn2  3773  pwsnALT  3822  unimax  3861  trss  4122  elssabg  4166  intabs  4172  nnullss  4235  exss  4236  fri  4355  onssmin  4588  tfis  4645  tfisi  4649  releq  4771  xpsspw  4797  iss  4998  relcnvtr  5192  fununi  5316  funcnvuni  5317  ffoss  5505  ssimaex  5584  isofrlem  5837  f1oweALT  5851  frxp  6225  tfrlem1  6391  oawordeu  6553  qsss  6720  boxcutc  6859  sbthlem2  6972  sbth  6981  php  7045  isinf  7076  unbnn2  7114  domunfican  7129  fiint  7133  finsschain  7162  indexfi  7163  dffi3  7184  hartogslem1  7257  sucprcreg  7313  cantnfval2  7370  cantnfle  7372  cantnflem1  7391  tz9.1  7411  setind  7419  tcvalg  7423  scott0  7556  bnd2  7563  carduni  7614  cardaleph  7716  alephinit  7722  aceq3lem  7747  dfac12lem3  7771  infmap2  7844  cflem  7872  cflm  7876  cflecard  7879  cfeq0  7882  cfsuc  7883  cfflb  7885  cfslb  7892  cfslb2n  7894  coftr  7899  fin23lem13  7958  fin23lem16  7961  fin23lem19  7962  fin23lem29  7967  fin1a2lem13  8038  itunitc  8047  domtriomlem  8068  axdc3lem2  8077  zorn2lem7  8129  zornn0g  8132  fpwwe2lem5  8256  pwfseqlem4a  8283  pwfseqlem4  8284  wunfi  8343  wunex2  8360  wuncval  8364  rankcf  8399  tskuni  8405  axgroth6  8450  axgroth3  8453  axgroth4  8454  fzoss1  10896  hashf1lem2  11394  sumeq1f  12161  fsumcvg3  12202  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  vdwmc  13025  restsspw  13336  ismred2  13505  mrcval  13512  mrcuni  13523  acsfn  13561  isssc  13697  drsdirfi  14072  clatlem  14216  clatl  14220  ipodrsima  14268  cntzssv  14804  isslw  14919  sylow2alem2  14929  sylow2a  14930  efgval  15026  gsumzaddlem  15203  ablfac1eulem  15307  lspval  15732  lspindpi  15885  aspval  16068  mplsubglem  16179  mpllsslem  16180  mplcoe1  16209  mplcoe2  16211  znf1o  16505  zntoslem  16510  uniopn  16643  fiinopn  16647  fiinbas  16690  baspartn  16692  eltg2  16696  eltg3  16700  topbas  16710  pptbas  16745  clsval  16774  neival  16839  neiint  16841  neips  16850  opnneissb  16851  opnssneib  16852  innei  16862  restbas  16889  restcld  16903  restcls  16911  restntr  16912  cnpdis  17021  nrmsep3  17083  cmpsublem  17126  cmpsub  17127  fiuncmp  17131  uncon  17155  1stcfb  17171  2ndc1stc  17177  1stcrest  17179  2ndcctbss  17181  2ndcomap  17184  dis2ndc  17186  lly1stc  17222  llycmpkgen2  17245  txbas  17262  eltx  17263  ptuni2  17271  ptpjopn  17306  ptcld  17307  txlm  17342  tx1stc  17344  txkgen  17346  xkopt  17349  xkococnlem  17353  ptcmpfi  17504  fbssfi  17532  opnfbas  17537  isfil2  17551  isfildlem  17552  snfil  17559  fsubbas  17562  ssfg  17567  fgss2  17569  fgcl  17573  fbasrn  17579  fgtr  17585  ufli  17609  uffix  17616  rnelfmlem  17647  fclscf  17720  alexsublem  17738  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  tmdgsum2  17779  subgntr  17789  opnsubg  17790  divstgpopn  17802  tsmsfbas  17810  tsmsgsum  17821  tsmsres  17826  tsmsf1o  17827  tsmsxplem1  17835  tsmsxp  17837  blssex  17973  neibl  18047  blcld  18051  met1stc  18067  met2ndci  18068  metrest  18070  prdsxmslem2  18075  dscopn  18096  isngp2  18119  tgioo  18302  tgqioo  18306  zdis  18322  xrge0tsms  18339  fsumcn  18374  ovolval  18833  volivth  18962  vitalilem2  18964  itgfsum  19181  limcun  19245  recnprss  19254  dvmptfsum  19322  ftc1a  19384  plyssc  19582  efopn  20005  jensen  20283  hhsssh  21846  shintcl  21909  chintcl  21911  spanval  21912  omlsi  21983  pjoml  22015  chnlen0  22023  chsscon3  22079  chlejb1  22091  chnle  22093  spanun  22124  h1datom  22161  cmbr4i  22180  pjoml2  22190  pjoml3  22191  lecm  22196  osumcor2i  22223  osum  22224  spansncv  22232  pjcjt2  22271  pjopyth  22299  pjss1coi  22743  hstel2  22799  stj  22815  stcltr1i  22854  mdi  22875  mdbr3  22877  mdbr4  22878  dmdbr  22879  dmdmd  22880  dmdbr5  22888  mdsl1i  22901  mdslmd1lem3  22907  mdslmd1lem4  22908  mdslmd1i  22909  csmdsymi  22914  atss  22926  atom1d  22933  superpos  22934  chcv1  22935  shatomici  22938  shatomistici  22941  hatomistici  22942  chrelat2  22950  chirredi  22974  atcvat4i  22977  mdsymlem2  22984  mdsymlem6  22988  dmdbr6ati  23003  dmdbr7ati  23004  tpr2rico  23296  xrge0tsmsd  23382  issiga  23472  isrnsigaOLD  23473  isrnsiga  23474  sigagenval  23501  measiuns  23544  dya2iocseg  23579  kur14lem1  23737  cvmopnlem  23809  rtrclreclem.min  24044  dfon2lem3  24141  dfon2lem7  24145  frmin  24242  wfrlem1  24256  wfrlem4  24259  wfrlem15  24270  frrlem1  24281  frrlem3  24283  brsset  24429  bpolyval  24784  onsucsuccmpi  24882  scprefat  25071  scprefat2  25072  twsymr  25078  imfstnrelc  25081  reflincror  25112  int2pre  25237  posprsr  25240  inposetlem  25276  inposet  25278  rninc  25281  ranncnt  25283  dfps2  25289  svs2  25487  svs3  25488  oibbi1  25509  oibbi2  25510  basexre  25522  sallnei  25529  osneisi  25531  intopcoaconlem3b  25538  intopcoaconlem3  25539  qusp  25542  efilcp  25552  prdnei  25573  altretop  25600  hdrmp  25706  infemb  25859  vtarsuelt  25895  indcls2  25996  isig12  26064  iscol2  26093  refssex  26281  fness  26282  fneref  26284  fnessref  26293  neibastop2lem  26309  topmeet  26313  fnejoin2  26318  tailfb  26326  filnetlem4  26330  indexa  26412  indexdom  26413  neificl  26467  istotbnd3  26495  sstotbnd2  26498  sstotbnd  26499  equivtotbnd  26502  ssbnd  26512  heiborlem1  26535  heiborlem6  26540  heiborlem8  26542  heiborlem10  26544  unichnidl  26656  pridl  26662  ismaxidl  26665  igenval  26686  igenval2  26691  ispridlc  26695  ismrcd1  26773  ismrcd2  26774  ismrc  26776  mzpcompact2lem  26829  aomclem6  27156  hbtlem6  27333  rgspnval  27373  pmtrfrn  27400  stoweidlem34  27783  stoweidlem51  27800  stoweidlem52  27801  prelpw  28074  usgraedgprv  28122  onfrALTlem5  28307  onfrALTlem5VD  28661  bnj1143  28822  bnj517  28917  bnj1118  29014  bnj1145  29023  bnj1154  29029  bnj1452  29082  bnj1498  29091  lsmsat  29198  lssatomic  29201  lssats  29202  lsat0cv  29223  lcvexchlem4  29227  lcvexchlem5  29228  lsatcvatlem  29239  l1cvpat  29244  ispsubsp  29934  linepsubN  29941  pclvalN  30079  ispsubclN  30126  ispsubcl2N  30136  pclfinclN  30139  diaelrnN  31235  docavalN  31313  dochval  31541  dvh4dimat  31628  dochexmidlem1  31650  lpolconN  31677  mapdordlem2  31827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator