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

Theorem unss 3362
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 3182 . 2  |-  ( ( A  u.  B ) 
C_  C  <->  A. x
( x  e.  ( A  u.  B )  ->  x  e.  C
) )
2 19.26 1583 . . 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 3329 . . . . . 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 1556 . . 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 3182 . . . 4  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
9 dfss2 3182 . . . 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 1530    e. wcel 1696    u. cun 3163    C_ wss 3165
This theorem is referenced by:  unssi  3363  unssd  3364  unssad  3365  unssbd  3366  nsspssun  3415  uneqin  3433  uneqdifeq  3555  prss  3785  prssg  3786  ssunsn2  3789  tpss  3795  pwundif  4316  eldifpw  4582  eqrelrel  4804  xpsspw  4813  xpsspwOLD  4814  relun  4818  relcoi2  5216  fnsuppres  5748  dfer2  6677  isinf  7092  fiin  7191  trcl  7426  supxrun  10650  isumltss  12323  rpnnen2  12520  lubun  14243  isipodrs  14280  fpwipodrs  14283  ipodrsima  14284  aspval2  16102  unocv  16596  uncld  16794  restntr  16928  cmpcld  17145  uncmp  17146  ufprim  17620  tsmsfbas  17826  ovolctb2  18867  ovolun  18874  unmbl  18911  mbfeqalem  19013  plyun0  19595  sshjcl  21950  sshjval2  22006  shlub  22009  ssjo  22042  spanuni  22139  pwundif2  23202  dfon2lem3  24212  dfon2lem7  24216  wfrlem15  24341  toplat  25393  cnfilca  25659  hdrmp  25809  pvp  26151  pgapspf  26155  clsun  26349  lsmfgcl  27275  lubunNEW  29785  paddssat  30625  pclunN  30709  paddunN  30738  poldmj1N  30739  pclfinclN  30761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator