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

Theorem sseq2 3362
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 3347 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 29 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3347 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 29 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 550 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3355 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 610 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 258 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
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  sseq2i  3365  sseq2d  3368  syl5sseq  3388  nssne1  3396  psseq2  3427  sseq0  3651  un00  3655  disjpss  3670  pweq  3794  ssintab  4059  ssintub  4060  intmin  4062  treq  4300  ssexg  4341  intabs  4353  ordunidif  4621  ordssun  4673  iunpw  4751  tfindsg  4832  limomss  4842  findsg  4864  fununi  5509  funcnvuni  5510  feq3  5570  ssimaexg  5781  frxp  6448  onfununi  6595  oawordeu  6790  oawordexr  6791  nnawordex  6872  ereq1  6904  xpider  6967  domeng  7114  sbthlem4  7212  sbthlem5  7213  domssex  7260  finsschain  7405  dffi2  7420  dffi3  7428  hartogslem1  7503  inf3lema  7571  cantnflem1  7637  tz9.1  7657  tz9.1c  7658  tctr  7671  tcmin  7672  tcrank  7800  scottex  7801  cardlim  7851  infxpenlem  7887  infxpenc2  7895  isinfcard  7965  alephinit  7968  alephval3  7983  dfac3  7994  cflem  8118  cfval  8119  cflecard  8125  cfsuc  8129  cff1  8130  cfflb  8131  cflim2  8135  isf32lem2  8226  fin1a2lem13  8284  ac7g  8346  ttukeylem5  8385  ttukeylem7  8387  pwcfsdom  8450  pwfseqlem5  8530  pwfseq  8531  gch2  8546  winalim  8562  wunex  8606  wuncss  8612  eltskg  8617  eltsk2g  8618  gruina  8685  grur1a  8686  axgroth6  8695  mrcflem  13823  mrcval  13827  isacs2  13870  acsfiel  13871  ipoval  14572  fpwipodrs  14582  ipodrsima  14583  mreclat  14605  slwispgp  15237  pgpssslw  15240  lsmss1b  15291  lsmss2b  15293  lspf  16042  lspval  16043  lbsextlem1  16222  lbsextlem3  16224  lbsextlem4  16225  aspval  16379  mplsubglem  16490  mpllsslem  16491  basis2  17008  eltg2  17015  clsval  17093  clscld  17103  clsval2  17106  ntrcls0  17132  isnei  17159  neiint  17160  neips  17169  opnneissb  17170  opnssneib  17171  neindisj2  17179  innei  17181  neiptoptop  17187  neiptopnei  17188  neitr  17236  restcls  17237  cnpimaex  17312  cnprest2  17346  regsep  17390  nrmsep3  17411  nrmsep  17413  regsep2  17432  tgcmp  17456  uncmp  17458  bwth  17465  1stcfb  17500  1stcrest  17508  2ndcctbss  17510  1stcelcls  17516  lly1stc  17551  xkoopn  17613  neitx  17631  txcnp  17644  txcmplem1  17665  kqnrmlem1  17767  kqnrmlem2  17768  nrmhmph  17818  fbssfi  17861  opnfbas  17866  fbasfip  17892  fbunfip  17893  fgss2  17898  fgcl  17902  supfil  17919  isufil2  17932  filssufilg  17935  ssufl  17942  ufileu  17943  elfm3  17974  fmfnfm  17982  ufldom  17986  fbflim2  18001  flfneii  18016  flftg  18020  txflf  18030  supnfcls  18044  fclscf  18049  fclsfnflim  18051  flimfnfcls  18052  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALTlem4  18073  alexsubALT  18074  tsmsfbas  18149  tsmsres  18165  tsmsf1o  18166  tsmsxplem1  18174  tsmsxp  18176  ustssel  18227  ustincl  18229  ustdiag  18230  ustinvel  18231  ustexhalf  18232  ust0  18241  elutop  18255  ustuqtop4  18266  cfiluexsm  18312  cfiluweak  18317  blssps  18446  blss  18447  metss  18530  metrest  18546  metcnp3  18562  metnrmlem3  18883  lebnumlem3  18980  lebnum  18981  ellimc3  19758  lhop1lem  19889  dchrelbas  21012  avril1  21749  resgrprn  21860  spanval  22827  spancl  22830  shsval2i  22881  omlsi  22898  ococin  22902  chsupsn  22907  pjoml  22930  shs00i  22944  chj00i  22981  chsscon3  22994  chlejb1  23006  chnle  23008  pjoml2  23105  pjoml3  23106  lecm  23111  stcltr1i  23769  mdbr  23789  dmdmd  23795  dmdi  23797  dmdbr3  23800  dmdbr4  23801  mdsl1i  23816  mdslmd1lem3  23822  mdslmd1lem4  23823  csmdsymi  23829  hatomic  23855  chrelat2  23865  atord  23883  atcvat4i  23892  sigagenval  24515  dmsigagen  24519  sigagenss  24524  kur14lem9  24892  dfrtrcl2  25140  fprodss  25266  wrecseq123  25524  wfrlem1  25530  wfrlem4  25533  wfrlem15  25544  frrlem1  25574  frrlem4  25577  frrlem5e  25582  frrlem11  25586  imagesset  25790  altopthsn  25798  mblfinlem2  26235  ssref  26344  refref  26346  fnessref  26354  refssfne  26355  comppfsc  26368  topjoin  26375  neifg  26381  totbndss  26467  heibor1lem  26499  unichnidl  26622  ispridl  26625  maxidlmax  26634  igenval  26652  igenidl  26654  igenmin  26655  igenval2  26657  nacsfix  26747  mzpcompact2  26790  rgspnval  27331  rgspncl  27332  rgspnmin  27334  ssrecnpr  27495  swrdvalodm2  28150  swrdvalodm  28151  bnj1286  29315  bnj1452  29348  lsatcmp  29728  lcvexchlem4  29762  lcvexchlem5  29763  pclvalN  30614  pclclN  30615  elpcliN  30617  docaclN  31849  dihglb2  32067  doch2val2  32089  dochocss  32091  dochexmidlem7  32191  lpolconN  32212  mapdval  32353
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