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

Theorem unss 3521
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 3337 . 2  |-  ( ( A  u.  B ) 
C_  C  <->  A. x
( x  e.  ( A  u.  B )  ->  x  e.  C
) )
2 19.26 1603 . . 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 3488 . . . . . 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 1575 . . 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 3337 . . . 4  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
9 dfss2 3337 . . . 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 1549    e. wcel 1725    u. cun 3318    C_ wss 3320
This theorem is referenced by:  unssi  3522  unssd  3523  unssad  3524  unssbd  3525  nsspssun  3574  uneqin  3592  uneqdifeq  3716  prss  3952  prssg  3953  ssunsn2  3958  tpss  3964  pwundif  4490  eqrelrel  4977  xpsspw  4986  xpsspwOLD  4987  relun  4991  relcoi2  5397  fnsuppres  5952  dfer2  6906  isinf  7322  fiin  7427  trcl  7664  supxrun  10894  isumltss  12628  rpnnen2  12825  lubun  14550  isipodrs  14587  fpwipodrs  14590  ipodrsima  14591  aspval2  16405  unocv  16907  uncld  17105  restntr  17246  cmpcld  17465  uncmp  17466  ufprim  17941  tsmsfbas  18157  ovolctb2  19388  ovolun  19395  unmbl  19432  plyun0  20116  sshjcl  22857  sshjval2  22913  shlub  22916  ssjo  22949  spanuni  23046  dfon2lem3  25412  dfon2lem7  25416  wfrlem15  25552  mblfinlem3  26245  ismblfin  26247  clsun  26331  lsmfgcl  27149  lubunNEW  29771  paddssat  30611  pclunN  30695  paddunN  30724  poldmj1N  30725  pclfinclN  30747
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-or 360  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-nfc 2561  df-v 2958  df-un 3325  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator