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

Theorem unss 3599
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 3407 . 2  |-  ( ( A  u.  B ) 
C_  C  <->  A. x
( x  e.  ( A  u.  B )  ->  x  e.  C
) )
2 19.26 1740 . . 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 3565 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
43imbi1i 332 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  ->  x  e.  C )  <->  ( ( x  e.  A  \/  x  e.  B
)  ->  x  e.  C ) )
5 jaob 800 . . . . 5  |-  ( ( ( x  e.  A  \/  x  e.  B
)  ->  x  e.  C )  <->  ( (
x  e.  A  ->  x  e.  C )  /\  ( x  e.  B  ->  x  e.  C ) ) )
64, 5bitri 257 . . . 4  |-  ( ( x  e.  ( A  u.  B )  ->  x  e.  C )  <->  ( ( x  e.  A  ->  x  e.  C )  /\  ( x  e.  B  ->  x  e.  C ) ) )
76albii 1699 . . 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 3407 . . . 4  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
9 dfss2 3407 . . . 4  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
108, 9anbi12i 711 . . 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 285 . 2  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  x  e.  C )  <->  ( A  C_  C  /\  B  C_  C ) )
121, 11bitr2i 258 1  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    \/ wo 375    /\ wa 376   A.wal 1450    e. wcel 1904    u. cun 3388    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395  df-in 3397  df-ss 3404
This theorem is referenced by:  unssi  3600  unssd  3601  unssad  3602  unssbd  3603  nsspssun  3667  uneqin  3685  uneqdifeq  3847  prss  4117  prssg  4118  ssunsn2  4123  tpss  4129  pwundif  4746  eqrelrel  4941  xpsspw  4953  relun  4955  relcoi2  5370  fnsuppres  6961  wfrlem15  7068  dfer2  7382  isinf  7803  fiin  7954  trcl  8230  supxrun  11626  trclun  13155  isumltss  13983  rpnnen2  14355  lcmfunsnlem  14693  lcmfun  14697  coprmprod  14757  coprmproddvdslem  14758  lubun  16447  isipodrs  16485  fpwipodrs  16488  ipodrsima  16489  aspval2  18648  unocv  19320  uncld  20133  restntr  20275  cmpcld  20494  uncmp  20495  ufprim  21002  tsmsfbas  21220  ovolctb2  22523  ovolun  22530  unmbl  22569  plyun0  23230  sshjcl  27089  sshjval2  27145  shlub  27148  ssjo  27181  spanuni  27278  dfon2lem3  30502  dfon2lem7  30506  clsun  31055  mblfinlem3  32043  ismblfin  32045  paddssat  33450  pclunN  33534  paddunN  33563  poldmj1N  33564  pclfinclN  33586  lsmfgcl  36003  ssuncl  36245  sssymdifcl  36247  undmrnresiss  36281  mptrcllem  36291  cnvrcl0  36303  dfrtrcl5  36307  brtrclfv2  36390  unhe1  36452  dffrege76  36606  iunopeqop  39151
  Copyright terms: Public domain W3C validator