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

Theorem unss 3310
Description: The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.)
Assertion
Ref Expression
unss  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)

Proof of Theorem unss
StepHypRef Expression
1 dfss2 3130 . 2  |-  ( ( A  u.  B ) 
C_  C  <->  A. x
( x  e.  ( A  u.  B )  ->  x  e.  C
) )
2 19.26 1592 . . 3  |-  ( A. x ( ( x  e.  A  ->  x  e.  C )  /\  (
x  e.  B  ->  x  e.  C )
)  <->  ( A. x
( x  e.  A  ->  x  e.  C )  /\  A. x ( x  e.  B  ->  x  e.  C )
) )
3 elun 3277 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
43imbi1i 317 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  ->  x  e.  C )  <->  ( ( x  e.  A  \/  x  e.  B
)  ->  x  e.  C ) )
5 jaob 761 . . . . 5  |-  ( ( ( x  e.  A  \/  x  e.  B
)  ->  x  e.  C )  <->  ( (
x  e.  A  ->  x  e.  C )  /\  ( x  e.  B  ->  x  e.  C ) ) )
64, 5bitri 242 . . . 4  |-  ( ( x  e.  ( A  u.  B )  ->  x  e.  C )  <->  ( ( x  e.  A  ->  x  e.  C )  /\  ( x  e.  B  ->  x  e.  C ) ) )
76albii 1554 . . 3  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  x  e.  C )  <->  A. x
( ( x  e.  A  ->  x  e.  C )  /\  (
x  e.  B  ->  x  e.  C )
) )
8 dfss2 3130 . . . 4  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
9 dfss2 3130 . . . 4  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
108, 9anbi12i 681 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A. x ( x  e.  A  ->  x  e.  C )  /\  A. x ( x  e.  B  ->  x  e.  C ) ) )
112, 7, 103bitr4i 270 . 2  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  x  e.  C )  <->  ( A  C_  C  /\  B  C_  C ) )
121, 11bitr2i 243 1  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    \/ wo 359    /\ wa 360   A.wal 1532    e. wcel 1621    u. cun 3111    C_ wss 3113
This theorem is referenced by:  unssi  3311  unssd  3312  unssad  3313  unssbd  3314  nsspssun  3363  uneqin  3381  uneqdifeq  3503  prss  3729  prssg  3730  ssunsn2  3733  tpss  3739  pwundif  4258  eldifpw  4524  eqrelrel  4762  xpsspw  4771  xpsspwOLD  4772  relun  4776  relcoi2  5173  fnsuppres  5652  dfer2  6615  isinf  7030  fiin  7129  trcl  7364  supxrun  10586  isumltss  12255  rpnnen2  12452  lubun  14175  isipodrs  14212  fpwipodrs  14215  ipodrsima  14216  aspval2  16034  unocv  16528  uncld  16726  restntr  16860  cmpcld  17077  uncmp  17078  ufprim  17552  tsmsfbas  17758  ovolctb2  18799  ovolun  18806  unmbl  18843  mbfeqalem  18945  plyun0  19527  sshjcl  21880  sshjval2  21936  shlub  21939  ssjo  21972  spanuni  22069  dfon2lem3  23496  dfon2lem7  23500  wfrlem15  23625  toplat  24643  cnfilca  24909  hdrmp  25059  pvp  25401  pgapspf  25405  clsun  25599  lsmfgcl  26525  lubunNEW  28314  paddssat  29154  pclunN  29238  paddunN  29267  poldmj1N  29268  pclfinclN  29290
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-un 3118  df-in 3120  df-ss 3127
  Copyright terms: Public domain W3C validator