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

Theorem unss 3457
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfss2 3273 . 2  |-  ( ( A  u.  B ) 
C_  C  <->  A. x
( x  e.  ( A  u.  B )  ->  x  e.  C
) )
2 19.26 1600 . . 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 3424 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
43imbi1i 316 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  ->  x  e.  C )  <->  ( ( x  e.  A  \/  x  e.  B
)  ->  x  e.  C ) )
5 jaob 759 . . . . 5  |-  ( ( ( x  e.  A  \/  x  e.  B
)  ->  x  e.  C )  <->  ( (
x  e.  A  ->  x  e.  C )  /\  ( x  e.  B  ->  x  e.  C ) ) )
64, 5bitri 241 . . . 4  |-  ( ( x  e.  ( A  u.  B )  ->  x  e.  C )  <->  ( ( x  e.  A  ->  x  e.  C )  /\  ( x  e.  B  ->  x  e.  C ) ) )
76albii 1572 . . 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 3273 . . . 4  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
9 dfss2 3273 . . . 4  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
108, 9anbi12i 679 . . 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 269 . 2  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  x  e.  C )  <->  ( A  C_  C  /\  B  C_  C ) )
121, 11bitr2i 242 1  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359   A.wal 1546    e. wcel 1717    u. cun 3254    C_ wss 3256
This theorem is referenced by:  unssi  3458  unssd  3459  unssad  3460  unssbd  3461  nsspssun  3510  uneqin  3528  uneqdifeq  3652  prss  3888  prssg  3889  ssunsn2  3894  tpss  3900  pwundif  4424  eqrelrel  4910  xpsspw  4919  xpsspwOLD  4920  relun  4924  relcoi2  5330  fnsuppres  5884  dfer2  6835  isinf  7251  fiin  7355  trcl  7590  supxrun  10819  isumltss  12548  rpnnen2  12745  lubun  14470  isipodrs  14507  fpwipodrs  14510  ipodrsima  14511  aspval2  16325  unocv  16823  uncld  17021  restntr  17161  cmpcld  17380  uncmp  17381  ufprim  17855  tsmsfbas  18071  ovolctb2  19248  ovolun  19255  unmbl  19292  plyun0  19976  constr2trl  21439  sshjcl  22698  sshjval2  22754  shlub  22757  ssjo  22790  spanuni  22887  dfon2lem3  25158  dfon2lem7  25162  wfrlem15  25287  clsun  26015  lsmfgcl  26834  lubunNEW  29139  paddssat  29979  pclunN  30063  paddunN  30092  poldmj1N  30093  pclfinclN  30115
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-un 3261  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator