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

Theorem sseq1 3361
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 3355 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
2 sstr2 3347 . . . 4  |-  ( B 
C_  A  ->  ( A  C_  C  ->  B  C_  C ) )
32adantl 453 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  ->  B  C_  C )
)
4 sstr2 3347 . . . 4  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
54adantr 452 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( B  C_  C  ->  A  C_  C )
)
63, 5impbid 184 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  <->  B 
C_  C ) )
71, 6sylbi 188 1  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    C_ wss 3312
This theorem is referenced by:  sseq12  3363  sseq1i  3364  sseq1d  3367  nssne2  3397  psseq1  3426  uneqdifeq  3708  sbss  3729  pwjust  3792  elpw  3797  elpwg  3798  pwpw0  3938  sssn  3949  ssunsn2  3950  pwsnALT  4002  unimax  4041  trss  4303  elssabg  4347  intabs  4353  nnullss  4417  exss  4418  fri  4536  onssmin  4769  tfis  4826  tfisi  4830  releq  4951  xpsspw  4978  iss  5181  relcnvtr  5381  fununi  5509  funcnvuni  5510  ffoss  5699  ssimaex  5780  isofrlem  6052  f1oweALT  6066  frxp  6448  tfrlem1  6628  oawordeu  6790  qsss  6957  boxcutc  7097  sbthlem2  7210  sbth  7219  php  7283  isinf  7314  unbnn2  7356  domunfican  7371  fiint  7375  finsschain  7405  indexfi  7406  dffi3  7428  hartogslem1  7503  sucprcreg  7559  cantnfval2  7616  cantnfle  7618  cantnflem1  7637  tz9.1  7657  setind  7665  tcvalg  7669  scott0  7802  bnd2  7809  carduni  7860  cardaleph  7962  alephinit  7968  aceq3lem  7993  dfac12lem3  8017  infmap2  8090  cflem  8118  cflm  8122  cflecard  8125  cfeq0  8128  cfsuc  8129  cfflb  8131  cfslb  8138  cfslb2n  8140  coftr  8145  fin23lem13  8204  fin23lem16  8207  fin23lem19  8208  fin23lem29  8213  fin1a2lem13  8284  itunitc  8293  domtriomlem  8314  axdc3lem2  8323  zorn2lem7  8374  zornn0g  8377  fpwwe2lem5  8501  pwfseqlem4a  8528  pwfseqlem4  8529  wunfi  8588  wunex2  8605  wuncval  8609  rankcf  8644  tskuni  8650  axgroth6  8695  axgroth3  8698  axgroth4  8699  fzoss1  11154  hashf1lem2  11697  sumeq1f  12474  fsumcvg3  12515  fsum2d  12547  fsumabs  12572  fsumrlim  12582  fsumo1  12583  fsumiun  12592  vdwmc  13338  restsspw  13651  ismred2  13820  mrcval  13827  mrcuni  13838  acsfn  13876  isssc  14012  drsdirfi  14387  clatlem  14531  clatl  14535  ipodrsima  14583  cntzssv  15119  isslw  15234  sylow2alem2  15244  sylow2a  15245  efgval  15341  gsumzaddlem  15518  ablfac1eulem  15622  lspval  16043  lspindpi  16196  aspval  16379  mplsubglem  16490  mpllsslem  16491  mplcoe1  16520  mplcoe2  16522  znf1o  16824  zntoslem  16829  uniopn  16962  fiinopn  16966  fiinbas  17009  baspartn  17011  eltg2  17015  eltg3  17019  topbas  17029  pptbas  17064  clsval  17093  neival  17158  neiint  17160  neips  17169  opnneissb  17170  opnssneib  17171  innei  17181  neiptoptop  17187  neiptopnei  17188  restbas  17214  restcld  17228  neitr  17236  restcls  17237  restntr  17238  cnpdis  17349  nrmsep3  17411  cmpsublem  17454  cmpsub  17455  fiuncmp  17459  uncon  17484  1stcfb  17500  2ndc1stc  17506  1stcrest  17508  2ndcctbss  17510  2ndcomap  17513  dis2ndc  17515  lly1stc  17551  llycmpkgen2  17574  txbas  17591  eltx  17592  ptuni2  17600  neitx  17631  ptpjopn  17636  ptcld  17637  txlm  17672  tx1stc  17674  txkgen  17676  xkopt  17679  xkococnlem  17683  ptcmpfi  17837  fbssfi  17861  opnfbas  17866  isfil2  17880  isfildlem  17881  snfil  17888  fsubbas  17891  ssfg  17896  fgss2  17898  fgcl  17902  fbasrn  17908  fgtr  17914  ufli  17938  uffix  17945  rnelfmlem  17976  fclscf  18049  alexsublem  18067  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALTlem4  18073  alexsubALT  18074  tmdgsum2  18118  subgntr  18128  opnsubg  18129  divstgpopn  18141  tsmsfbas  18149  tsmsgsum  18160  tsmsres  18165  tsmsf1o  18166  tsmsxplem1  18174  tsmsxp  18176  isust  18225  ustssel  18227  ustincl  18229  ustdiag  18230  ustinvel  18231  ustexhalf  18232  ustexsym  18237  ust0  18241  restutop  18259  ustuqtop4  18266  utopsnneiplem  18269  blssexps  18448  blssex  18449  neibl  18523  blcld  18527  met1stc  18543  met2ndci  18544  metrest  18546  prdsxmslem2  18551  metustfbasOLD  18587  metustfbas  18588  cfilucfilOLD  18591  cfilucfil  18592  metuel2  18601  metustblOLD  18602  metustbl  18603  restmetu  18609  dscopn  18613  isngp2  18636  tgioo  18819  tgqioo  18823  zdis  18839  xrge0tsms  18857  fsumcn  18892  ovolval  19362  volivth  19491  vitalilem2  19493  itgfsum  19710  limcun  19774  recnprss  19783  dvmptfsum  19851  ftc1a  19913  plyssc  20111  efopn  20541  jensen  20819  usgraedgprv  21388  hhsssh  22761  shintcl  22824  chintcl  22826  spanval  22827  omlsi  22898  pjoml  22930  chnlen0  22938  chsscon3  22994  chlejb1  23006  chnle  23008  spanun  23039  h1datom  23076  cmbr4i  23095  pjoml2  23105  pjoml3  23106  lecm  23111  osumcor2i  23138  osum  23139  spansncv  23147  pjcjt2  23186  pjopyth  23214  hstel2  23714  stj  23730  stcltr1i  23769  mdi  23790  mdbr3  23792  mdbr4  23793  dmdbr  23794  dmdmd  23795  dmdbr5  23803  mdsl1i  23816  mdslmd1lem3  23822  mdslmd1lem4  23823  mdslmd1i  23824  csmdsymi  23829  atss  23841  atom1d  23848  superpos  23849  chcv1  23850  shatomici  23853  shatomistici  23856  hatomistici  23857  chrelat2  23865  chirredi  23889  atcvat4i  23892  mdsymlem2  23899  mdsymlem6  23903  dmdbr6ati  23918  dmdbr7ati  23919  xrge0tsmsd  24215  tpr2rico  24302  issiga  24486  isrnsigaOLD  24487  isrnsiga  24488  sigagenval  24515  measiuns  24563  dya2icoseg  24619  dya2iocnrect  24623  dya2iocuni  24625  kur14lem1  24884  cvmopnlem  24957  rtrclreclem.min  25139  prodeq1f  25226  fprod2d  25297  dfon2lem3  25404  dfon2lem7  25408  frmin  25509  wfrlem1  25530  wfrlem4  25533  wfrlem15  25544  frrlem1  25574  frrlem3  25576  brsset  25726  onsucsuccmpi  26185  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  refssex  26352  fness  26353  fneref  26355  fnessref  26364  neibastop2lem  26380  topmeet  26384  fnejoin2  26389  tailfb  26397  filnetlem4  26401  indexa  26426  indexdom  26427  neificl  26450  istotbnd3  26471  sstotbnd2  26474  sstotbnd  26475  equivtotbnd  26478  ssbnd  26488  heiborlem1  26511  heiborlem6  26516  heiborlem8  26518  heiborlem10  26520  unichnidl  26632  pridl  26638  ismaxidl  26641  igenval  26662  igenval2  26667  ispridlc  26671  ismrcd1  26743  ismrcd2  26744  ismrc  26746  mzpcompact2lem  26799  aomclem6  27125  hbtlem6  27301  rgspnval  27341  pmtrfrn  27368  stoweidlem51  27767  stoweidlem52  27768  frisusgranb  28324  onfrALTlem5  28565  onfrALTlem5VD  28934  bnj517  29193  bnj1118  29290  bnj1145  29299  bnj1154  29305  bnj1452  29358  bnj1498  29367  lsmsat  29743  lssatomic  29746  lssats  29747  lsat0cv  29768  lcvexchlem4  29772  lcvexchlem5  29773  lsatcvatlem  29784  l1cvpat  29789  ispsubsp  30479  linepsubN  30486  pclvalN  30624  ispsubclN  30671  ispsubcl2N  30681  pclfinclN  30684  diaelrnN  31780  docavalN  31858  dochval  32086  dvh4dimat  32173  dochexmidlem1  32195  lpolconN  32222  mapdordlem2  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator