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

Theorem sseq2 3356
Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
Assertion
Ref Expression
sseq2  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )

Proof of Theorem sseq2
StepHypRef Expression
1 sstr2 3341 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 30 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3341 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 30 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 551 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3349 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 611 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 259 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    C_ wss 3306
This theorem is referenced by:  sseq12  3357  sseq2i  3359  sseq2d  3362  syl5sseq  3382  nssne1  3390  psseq2  3421  sseq0  3644  un00  3687  disjpss  3702  pweq  3826  ssintab  4091  ssintub  4092  intmin  4094  treq  4333  ssexg  4378  intabs  4390  ordunidif  4658  ordssun  4710  iunpw  4788  tfindsg  4869  limomss  4879  findsg  4901  fununi  5546  funcnvuni  5547  feq3  5607  ssimaexg  5818  frxp  6485  onfununi  6632  oawordeu  6827  oawordexr  6828  nnawordex  6909  ereq1  6941  xpider  7004  domeng  7151  sbthlem4  7249  sbthlem5  7250  domssex  7297  finsschain  7442  dffi2  7457  dffi3  7465  hartogslem1  7540  inf3lema  7608  cantnflem1  7674  tz9.1  7694  tz9.1c  7695  tctr  7708  tcmin  7709  tcrank  7839  scottex  7840  cardlim  7890  infxpenlem  7926  infxpenc2  7934  isinfcard  8004  alephinit  8007  alephval3  8022  dfac3  8033  cflem  8157  cfval  8158  cflecard  8164  cfsuc  8168  cff1  8169  cfflb  8170  cflim2  8174  isf32lem2  8265  fin1a2lem13  8323  ac7g  8385  ttukeylem5  8424  ttukeylem7  8426  pwcfsdom  8489  pwfseqlem5  8569  pwfseq  8570  gch2  8581  winalim  8601  wunex  8645  wuncss  8651  eltskg  8656  eltsk2g  8657  gruina  8724  grur1a  8725  axgroth6  8734  mrcflem  13862  mrcval  13866  isacs2  13909  acsfiel  13910  ipoval  14611  fpwipodrs  14621  ipodrsima  14622  mreclat  14644  slwispgp  15276  pgpssslw  15279  lsmss1b  15330  lsmss2b  15332  lspf  16081  lspval  16082  lbsextlem1  16261  lbsextlem3  16263  lbsextlem4  16264  aspval  16418  mplsubglem  16529  mpllsslem  16530  basis2  17047  eltg2  17054  clsval  17132  clscld  17142  clsval2  17145  ntrcls0  17171  isnei  17198  neiint  17199  neips  17208  opnneissb  17209  opnssneib  17210  neindisj2  17218  innei  17220  neiptoptop  17226  neiptopnei  17227  neitr  17275  restcls  17276  cnpimaex  17351  cnprest2  17385  regsep  17429  nrmsep3  17450  nrmsep  17452  regsep2  17471  tgcmp  17495  uncmp  17497  bwth  17504  1stcfb  17539  1stcrest  17547  2ndcctbss  17549  1stcelcls  17555  lly1stc  17590  xkoopn  17652  neitx  17670  txcnp  17683  txcmplem1  17704  kqnrmlem1  17806  kqnrmlem2  17807  nrmhmph  17857  fbssfi  17900  opnfbas  17905  fbasfip  17931  fbunfip  17932  fgss2  17937  fgcl  17941  supfil  17958  isufil2  17971  filssufilg  17974  ssufl  17981  ufileu  17982  elfm3  18013  fmfnfm  18021  ufldom  18025  fbflim2  18040  flfneii  18055  flftg  18059  txflf  18069  supnfcls  18083  fclscf  18088  fclsfnflim  18090  flimfnfcls  18091  alexsubALTlem2  18110  alexsubALTlem3  18111  alexsubALTlem4  18112  alexsubALT  18113  tsmsfbas  18188  tsmsres  18204  tsmsf1o  18205  tsmsxplem1  18213  tsmsxp  18215  ustssel  18266  ustincl  18268  ustdiag  18269  ustinvel  18270  ustexhalf  18271  ust0  18280  elutop  18294  ustuqtop4  18305  cfiluexsm  18351  cfiluweak  18356  blssps  18485  blss  18486  metss  18569  metrest  18585  metcnp3  18601  metnrmlem3  18922  lebnumlem3  19019  lebnum  19020  ellimc3  19797  lhop1lem  19928  dchrelbas  21051  avril1  21788  resgrprn  21899  spanval  22866  spancl  22869  shsval2i  22920  omlsi  22937  ococin  22941  chsupsn  22946  pjoml  22969  shs00i  22983  chj00i  23020  chsscon3  23033  chlejb1  23045  chnle  23047  pjoml2  23144  pjoml3  23145  lecm  23150  stcltr1i  23808  mdbr  23828  dmdmd  23834  dmdi  23836  dmdbr3  23839  dmdbr4  23840  mdsl1i  23855  mdslmd1lem3  23861  mdslmd1lem4  23862  csmdsymi  23868  hatomic  23894  chrelat2  23904  atord  23922  atcvat4i  23931  sigagenval  24554  dmsigagen  24558  sigagenss  24563  kur14lem9  24931  dfrtrcl2  25179  fprodss  25305  wrecseq123  25563  wfrlem1  25569  wfrlem4  25572  wfrlem15  25583  frrlem1  25613  frrlem4  25616  frrlem5e  25621  frrlem11  25625  imagesset  25829  altopthsn  25837  mblfinlem3  26281  ssref  26401  refref  26403  fnessref  26411  refssfne  26412  comppfsc  26425  topjoin  26432  neifg  26438  totbndss  26524  heibor1lem  26556  unichnidl  26679  ispridl  26682  maxidlmax  26691  igenval  26709  igenidl  26711  igenmin  26712  igenval2  26714  nacsfix  26804  mzpcompact2  26847  rgspnval  27388  rgspncl  27389  rgspnmin  27391  ssrecnpr  27552  swrdvalodm2  28246  swrdvalodm  28247  bnj1286  29486  bnj1452  29519  lsatcmp  29899  lcvexchlem4  29933  lcvexchlem5  29934  pclvalN  30785  pclclN  30786  elpcliN  30788  docaclN  32020  dihglb2  32238  doch2val2  32260  dochocss  32262  dochexmidlem7  32362  lpolconN  32383  mapdval  32524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3313  df-ss 3320
  Copyright terms: Public domain W3C validator