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

Theorem sseq1 3212
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 3207 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
2 sstr2 3199 . . . 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 3199 . . . 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 1632    C_ wss 3165
This theorem is referenced by:  sseq12  3214  sseq1i  3215  sseq1d  3218  nssne2  3248  psseq1  3276  uneqdifeq  3555  sbss  3576  pwjust  3639  elpw  3644  elpwg  3645  pwpw0  3779  sssn  3788  ssunsn2  3789  pwsnALT  3838  unimax  3877  trss  4138  elssabg  4182  intabs  4188  nnullss  4251  exss  4252  fri  4371  onssmin  4604  tfis  4661  tfisi  4665  releq  4787  xpsspw  4813  iss  5014  relcnvtr  5208  fununi  5332  funcnvuni  5333  ffoss  5521  ssimaex  5600  isofrlem  5853  f1oweALT  5867  frxp  6241  tfrlem1  6407  oawordeu  6569  qsss  6736  boxcutc  6875  sbthlem2  6988  sbth  6997  php  7061  isinf  7092  unbnn2  7130  domunfican  7145  fiint  7149  finsschain  7178  indexfi  7179  dffi3  7200  hartogslem1  7273  sucprcreg  7329  cantnfval2  7386  cantnfle  7388  cantnflem1  7407  tz9.1  7427  setind  7435  tcvalg  7439  scott0  7572  bnd2  7579  carduni  7630  cardaleph  7732  alephinit  7738  aceq3lem  7763  dfac12lem3  7787  infmap2  7860  cflem  7888  cflm  7892  cflecard  7895  cfeq0  7898  cfsuc  7899  cfflb  7901  cfslb  7908  cfslb2n  7910  coftr  7915  fin23lem13  7974  fin23lem16  7977  fin23lem19  7978  fin23lem29  7983  fin1a2lem13  8054  itunitc  8063  domtriomlem  8084  axdc3lem2  8093  zorn2lem7  8145  zornn0g  8148  fpwwe2lem5  8272  pwfseqlem4a  8299  pwfseqlem4  8300  wunfi  8359  wunex2  8376  wuncval  8380  rankcf  8415  tskuni  8421  axgroth6  8466  axgroth3  8469  axgroth4  8470  fzoss1  10912  hashf1lem2  11410  sumeq1f  12177  fsumcvg3  12218  fsum2d  12250  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  vdwmc  13041  restsspw  13352  ismred2  13521  mrcval  13528  mrcuni  13539  acsfn  13577  isssc  13713  drsdirfi  14088  clatlem  14232  clatl  14236  ipodrsima  14284  cntzssv  14820  isslw  14935  sylow2alem2  14945  sylow2a  14946  efgval  15042  gsumzaddlem  15219  ablfac1eulem  15323  lspval  15748  lspindpi  15901  aspval  16084  mplsubglem  16195  mpllsslem  16196  mplcoe1  16225  mplcoe2  16227  znf1o  16521  zntoslem  16526  uniopn  16659  fiinopn  16663  fiinbas  16706  baspartn  16708  eltg2  16712  eltg3  16716  topbas  16726  pptbas  16761  clsval  16790  neival  16855  neiint  16857  neips  16866  opnneissb  16867  opnssneib  16868  innei  16878  restbas  16905  restcld  16919  restcls  16927  restntr  16928  cnpdis  17037  nrmsep3  17099  cmpsublem  17142  cmpsub  17143  fiuncmp  17147  uncon  17171  1stcfb  17187  2ndc1stc  17193  1stcrest  17195  2ndcctbss  17197  2ndcomap  17200  dis2ndc  17202  lly1stc  17238  llycmpkgen2  17261  txbas  17278  eltx  17279  ptuni2  17287  ptpjopn  17322  ptcld  17323  txlm  17358  tx1stc  17360  txkgen  17362  xkopt  17365  xkococnlem  17369  ptcmpfi  17520  fbssfi  17548  opnfbas  17553  isfil2  17567  isfildlem  17568  snfil  17575  fsubbas  17578  ssfg  17583  fgss2  17585  fgcl  17589  fbasrn  17595  fgtr  17601  ufli  17625  uffix  17632  rnelfmlem  17663  fclscf  17736  alexsublem  17754  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  tmdgsum2  17795  subgntr  17805  opnsubg  17806  divstgpopn  17818  tsmsfbas  17826  tsmsgsum  17837  tsmsres  17842  tsmsf1o  17843  tsmsxplem1  17851  tsmsxp  17853  blssex  17989  neibl  18063  blcld  18067  met1stc  18083  met2ndci  18084  metrest  18086  prdsxmslem2  18091  dscopn  18112  isngp2  18135  tgioo  18318  tgqioo  18322  zdis  18338  xrge0tsms  18355  fsumcn  18390  ovolval  18849  volivth  18978  vitalilem2  18980  itgfsum  19197  limcun  19261  recnprss  19270  dvmptfsum  19338  ftc1a  19400  plyssc  19598  efopn  20021  jensen  20299  hhsssh  21862  shintcl  21925  chintcl  21927  spanval  21928  omlsi  21999  pjoml  22031  chnlen0  22039  chsscon3  22095  chlejb1  22107  chnle  22109  spanun  22140  h1datom  22177  cmbr4i  22196  pjoml2  22206  pjoml3  22207  lecm  22212  osumcor2i  22239  osum  22240  spansncv  22248  pjcjt2  22287  pjopyth  22315  pjss1coi  22759  hstel2  22815  stj  22831  stcltr1i  22870  mdi  22891  mdbr3  22893  mdbr4  22894  dmdbr  22895  dmdmd  22896  dmdbr5  22904  mdsl1i  22917  mdslmd1lem3  22923  mdslmd1lem4  22924  mdslmd1i  22925  csmdsymi  22930  atss  22942  atom1d  22949  superpos  22950  chcv1  22951  shatomici  22954  shatomistici  22957  hatomistici  22958  chrelat2  22966  chirredi  22990  atcvat4i  22993  mdsymlem2  23000  mdsymlem6  23004  dmdbr6ati  23019  dmdbr7ati  23020  tpr2rico  23311  xrge0tsmsd  23397  issiga  23487  isrnsigaOLD  23488  isrnsiga  23489  sigagenval  23516  measiuns  23559  dya2iocseg  23594  kur14lem1  23752  cvmopnlem  23824  rtrclreclem.min  24059  cprodeq1f  24130  dfon2lem3  24212  dfon2lem7  24216  frmin  24313  wfrlem1  24327  wfrlem4  24330  wfrlem15  24341  frrlem1  24352  frrlem3  24354  brsset  24500  bpolyval  24856  onsucsuccmpi  24954  ovoliunnfl  25001  scprefat  25174  scprefat2  25175  twsymr  25181  imfstnrelc  25184  reflincror  25215  int2pre  25340  posprsr  25343  inposetlem  25379  inposet  25381  rninc  25384  ranncnt  25386  dfps2  25392  svs2  25590  svs3  25591  oibbi1  25612  oibbi2  25613  basexre  25625  sallnei  25632  osneisi  25634  intopcoaconlem3b  25641  intopcoaconlem3  25642  qusp  25645  efilcp  25655  prdnei  25676  altretop  25703  hdrmp  25809  infemb  25962  vtarsuelt  25998  indcls2  26099  isig12  26167  iscol2  26196  refssex  26384  fness  26385  fneref  26387  fnessref  26396  neibastop2lem  26412  topmeet  26416  fnejoin2  26421  tailfb  26429  filnetlem4  26433  indexa  26515  indexdom  26516  neificl  26570  istotbnd3  26598  sstotbnd2  26601  sstotbnd  26602  equivtotbnd  26605  ssbnd  26615  heiborlem1  26638  heiborlem6  26643  heiborlem8  26645  heiborlem10  26647  unichnidl  26759  pridl  26765  ismaxidl  26768  igenval  26789  igenval2  26794  ispridlc  26798  ismrcd1  26876  ismrcd2  26877  ismrc  26879  mzpcompact2lem  26932  aomclem6  27259  hbtlem6  27436  rgspnval  27476  pmtrfrn  27503  stoweidlem34  27886  stoweidlem51  27903  stoweidlem52  27904  prelpw  28184  usgraedgprv  28256  onfrALTlem5  28606  onfrALTlem5VD  28977  bnj1143  29138  bnj517  29233  bnj1118  29330  bnj1145  29339  bnj1154  29345  bnj1452  29398  bnj1498  29407  lsmsat  29820  lssatomic  29823  lssats  29824  lsat0cv  29845  lcvexchlem4  29849  lcvexchlem5  29850  lsatcvatlem  29861  l1cvpat  29866  ispsubsp  30556  linepsubN  30563  pclvalN  30701  ispsubclN  30748  ispsubcl2N  30758  pclfinclN  30761  diaelrnN  31857  docavalN  31935  dochval  32163  dvh4dimat  32250  dochexmidlem1  32272  lpolconN  32299  mapdordlem2  32449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator