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

Theorem sseq2 3370
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 3355 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 29 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3355 . . . 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 3363 . 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 3320
This theorem is referenced by:  sseq12  3371  sseq2i  3373  sseq2d  3376  syl5sseq  3396  nssne1  3404  psseq2  3435  sseq0  3659  un00  3663  disjpss  3678  pweq  3802  ssintab  4067  ssintub  4068  intmin  4070  treq  4308  ssexg  4349  intabs  4361  ordunidif  4629  ordssun  4681  iunpw  4759  tfindsg  4840  limomss  4850  findsg  4872  fununi  5517  funcnvuni  5518  feq3  5578  ssimaexg  5789  frxp  6456  onfununi  6603  oawordeu  6798  oawordexr  6799  nnawordex  6880  ereq1  6912  xpider  6975  domeng  7122  sbthlem4  7220  sbthlem5  7221  domssex  7268  finsschain  7413  dffi2  7428  dffi3  7436  hartogslem1  7511  inf3lema  7579  cantnflem1  7645  tz9.1  7665  tz9.1c  7666  tctr  7679  tcmin  7680  tcrank  7808  scottex  7809  cardlim  7859  infxpenlem  7895  infxpenc2  7903  isinfcard  7973  alephinit  7976  alephval3  7991  dfac3  8002  cflem  8126  cfval  8127  cflecard  8133  cfsuc  8137  cff1  8138  cfflb  8139  cflim2  8143  isf32lem2  8234  fin1a2lem13  8292  ac7g  8354  ttukeylem5  8393  ttukeylem7  8395  pwcfsdom  8458  pwfseqlem5  8538  pwfseq  8539  gch2  8554  winalim  8570  wunex  8614  wuncss  8620  eltskg  8625  eltsk2g  8626  gruina  8693  grur1a  8694  axgroth6  8703  mrcflem  13831  mrcval  13835  isacs2  13878  acsfiel  13879  ipoval  14580  fpwipodrs  14590  ipodrsima  14591  mreclat  14613  slwispgp  15245  pgpssslw  15248  lsmss1b  15299  lsmss2b  15301  lspf  16050  lspval  16051  lbsextlem1  16230  lbsextlem3  16232  lbsextlem4  16233  aspval  16387  mplsubglem  16498  mpllsslem  16499  basis2  17016  eltg2  17023  clsval  17101  clscld  17111  clsval2  17114  ntrcls0  17140  isnei  17167  neiint  17168  neips  17177  opnneissb  17178  opnssneib  17179  neindisj2  17187  innei  17189  neiptoptop  17195  neiptopnei  17196  neitr  17244  restcls  17245  cnpimaex  17320  cnprest2  17354  regsep  17398  nrmsep3  17419  nrmsep  17421  regsep2  17440  tgcmp  17464  uncmp  17466  bwth  17473  1stcfb  17508  1stcrest  17516  2ndcctbss  17518  1stcelcls  17524  lly1stc  17559  xkoopn  17621  neitx  17639  txcnp  17652  txcmplem1  17673  kqnrmlem1  17775  kqnrmlem2  17776  nrmhmph  17826  fbssfi  17869  opnfbas  17874  fbasfip  17900  fbunfip  17901  fgss2  17906  fgcl  17910  supfil  17927  isufil2  17940  filssufilg  17943  ssufl  17950  ufileu  17951  elfm3  17982  fmfnfm  17990  ufldom  17994  fbflim2  18009  flfneii  18024  flftg  18028  txflf  18038  supnfcls  18052  fclscf  18057  fclsfnflim  18059  flimfnfcls  18060  alexsubALTlem2  18079  alexsubALTlem3  18080  alexsubALTlem4  18081  alexsubALT  18082  tsmsfbas  18157  tsmsres  18173  tsmsf1o  18174  tsmsxplem1  18182  tsmsxp  18184  ustssel  18235  ustincl  18237  ustdiag  18238  ustinvel  18239  ustexhalf  18240  ust0  18249  elutop  18263  ustuqtop4  18274  cfiluexsm  18320  cfiluweak  18325  blssps  18454  blss  18455  metss  18538  metrest  18554  metcnp3  18570  metnrmlem3  18891  lebnumlem3  18988  lebnum  18989  ellimc3  19766  lhop1lem  19897  dchrelbas  21020  avril1  21757  resgrprn  21868  spanval  22835  spancl  22838  shsval2i  22889  omlsi  22906  ococin  22910  chsupsn  22915  pjoml  22938  shs00i  22952  chj00i  22989  chsscon3  23002  chlejb1  23014  chnle  23016  pjoml2  23113  pjoml3  23114  lecm  23119  stcltr1i  23777  mdbr  23797  dmdmd  23803  dmdi  23805  dmdbr3  23808  dmdbr4  23809  mdsl1i  23824  mdslmd1lem3  23830  mdslmd1lem4  23831  csmdsymi  23837  hatomic  23863  chrelat2  23873  atord  23891  atcvat4i  23900  sigagenval  24523  dmsigagen  24527  sigagenss  24532  kur14lem9  24900  dfrtrcl2  25148  fprodss  25274  wrecseq123  25532  wfrlem1  25538  wfrlem4  25541  wfrlem15  25552  frrlem1  25582  frrlem4  25585  frrlem5e  25590  frrlem11  25594  imagesset  25798  altopthsn  25806  mblfinlem3  26245  ssref  26363  refref  26365  fnessref  26373  refssfne  26374  comppfsc  26387  topjoin  26394  neifg  26400  totbndss  26486  heibor1lem  26518  unichnidl  26641  ispridl  26644  maxidlmax  26653  igenval  26671  igenidl  26673  igenmin  26674  igenval2  26676  nacsfix  26766  mzpcompact2  26809  rgspnval  27350  rgspncl  27351  rgspnmin  27353  ssrecnpr  27514  swrdvalodm2  28188  swrdvalodm  28189  bnj1286  29388  bnj1452  29421  lsatcmp  29801  lcvexchlem4  29835  lcvexchlem5  29836  pclvalN  30687  pclclN  30688  elpcliN  30690  docaclN  31922  dihglb2  32140  doch2val2  32162  dochocss  32164  dochexmidlem7  32264  lpolconN  32285  mapdval  32426
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator