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

Theorem unss 3349
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 3169 . 2  |-  ( ( A  u.  B ) 
C_  C  <->  A. x
( x  e.  ( A  u.  B )  ->  x  e.  C
) )
2 19.26 1580 . . 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 3316 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
43imbi1i 315 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  ->  x  e.  C )  <->  ( ( x  e.  A  \/  x  e.  B
)  ->  x  e.  C ) )
5 jaob 758 . . . . 5  |-  ( ( ( x  e.  A  \/  x  e.  B
)  ->  x  e.  C )  <->  ( (
x  e.  A  ->  x  e.  C )  /\  ( x  e.  B  ->  x  e.  C ) ) )
64, 5bitri 240 . . . 4  |-  ( ( x  e.  ( A  u.  B )  ->  x  e.  C )  <->  ( ( x  e.  A  ->  x  e.  C )  /\  ( x  e.  B  ->  x  e.  C ) ) )
76albii 1553 . . 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 3169 . . . 4  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
9 dfss2 3169 . . . 4  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
108, 9anbi12i 678 . . 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 268 . 2  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  x  e.  C )  <->  ( A  C_  C  /\  B  C_  C ) )
121, 11bitr2i 241 1  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358   A.wal 1527    e. wcel 1684    u. cun 3150    C_ wss 3152
This theorem is referenced by:  unssi  3350  unssd  3351  unssad  3352  unssbd  3353  nsspssun  3402  uneqin  3420  uneqdifeq  3542  prss  3769  prssg  3770  ssunsn2  3773  tpss  3779  pwundif  4300  eldifpw  4566  eqrelrel  4788  xpsspw  4797  xpsspwOLD  4798  relun  4802  relcoi2  5200  fnsuppres  5732  dfer2  6661  isinf  7076  fiin  7175  trcl  7410  supxrun  10634  isumltss  12307  rpnnen2  12504  lubun  14227  isipodrs  14264  fpwipodrs  14267  ipodrsima  14268  aspval2  16086  unocv  16580  uncld  16778  restntr  16912  cmpcld  17129  uncmp  17130  ufprim  17604  tsmsfbas  17810  ovolctb2  18851  ovolun  18858  unmbl  18895  mbfeqalem  18997  plyun0  19579  sshjcl  21934  sshjval2  21990  shlub  21993  ssjo  22026  spanuni  22123  pwundif2  23186  dfon2lem3  24141  dfon2lem7  24145  wfrlem15  24270  toplat  25290  cnfilca  25556  hdrmp  25706  pvp  26048  pgapspf  26052  clsun  26246  lsmfgcl  27172  lubunNEW  29163  paddssat  30003  pclunN  30087  paddunN  30116  poldmj1N  30117  pclfinclN  30139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator