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

Theorem unss 3351
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
)
Dummy variable  x is distinct from all other variables.

Proof of Theorem unss
StepHypRef Expression
1 dfss2 3171 . 2  |-  ( ( A  u.  B ) 
C_  C  <->  A. x
( x  e.  ( A  u.  B )  ->  x  e.  C
) )
2 19.26 1581 . . 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 3318 . . . . . 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 760 . . . . 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 3171 . . . 4  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
9 dfss2 3171 . . . 4  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
108, 9anbi12i 680 . . 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 1528    e. wcel 1685    u. cun 3152    C_ wss 3154
This theorem is referenced by:  unssi  3352  unssd  3353  unssad  3354  unssbd  3355  nsspssun  3404  uneqin  3422  uneqdifeq  3544  prss  3771  prssg  3772  ssunsn2  3775  tpss  3781  pwundif  4300  eldifpw  4566  eqrelrel  4788  xpsspw  4797  xpsspwOLD  4798  relun  4802  relcoi2  5199  fnsuppres  5694  dfer2  6657  isinf  7072  fiin  7171  trcl  7406  supxrun  10629  isumltss  12302  rpnnen2  12499  lubun  14222  isipodrs  14259  fpwipodrs  14262  ipodrsima  14263  aspval2  16081  unocv  16575  uncld  16773  restntr  16907  cmpcld  17124  uncmp  17125  ufprim  17599  tsmsfbas  17805  ovolctb2  18846  ovolun  18853  unmbl  18890  mbfeqalem  18992  plyun0  19574  sshjcl  21927  sshjval2  21983  shlub  21986  ssjo  22019  spanuni  22116  dfon2lem3  23543  dfon2lem7  23547  wfrlem15  23672  toplat  24690  cnfilca  24956  hdrmp  25106  pvp  25448  pgapspf  25452  clsun  25646  lsmfgcl  26572  lubunNEW  28431  paddssat  29271  pclunN  29355  paddunN  29384  poldmj1N  29385  pclfinclN  29407
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-un 3159  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator