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

Theorem ssequn1 3358
Description: A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
ssequn1  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )

Proof of Theorem ssequn1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 bicom 191 . . . 4  |-  ( ( x  e.  B  <->  ( x  e.  A  \/  x  e.  B ) )  <->  ( (
x  e.  A  \/  x  e.  B )  <->  x  e.  B ) )
2 pm4.72 846 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  B  <->  ( x  e.  A  \/  x  e.  B ) ) )
3 elun 3329 . . . . 5  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
43bibi1i 305 . . . 4  |-  ( ( x  e.  ( A  u.  B )  <->  x  e.  B )  <->  ( (
x  e.  A  \/  x  e.  B )  <->  x  e.  B ) )
51, 2, 43bitr4i 268 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  ( A  u.  B )  <->  x  e.  B ) )
65albii 1556 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x
( x  e.  ( A  u.  B )  <-> 
x  e.  B ) )
7 dfss2 3182 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
8 dfcleq 2290 . 2  |-  ( ( A  u.  B )  =  B  <->  A. x
( x  e.  ( A  u.  B )  <-> 
x  e.  B ) )
96, 7, 83bitr4i 268 1  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357   A.wal 1530    = wceq 1632    e. wcel 1696    u. cun 3163    C_ wss 3165
This theorem is referenced by:  ssequn2  3361  undif  3547  uniop  4285  pwssun  4315  unisuc  4484  ordssun  4508  ordequn  4509  onun2i  4524  ordunpr  4633  onuninsuci  4647  funiunfv  5790  sorpssun  6300  domss2  7036  sucdom2  7073  findcard2s  7115  rankopb  7540  ranksuc  7553  kmlem11  7802  fin1a2lem10  8051  cvgcmpce  12292  mreexexlem3d  13564  dprd2da  15293  dpjcntz  15303  dpjdisj  15304  dpjlsm  15305  dpjidcl  15309  ablfac1eu  15324  perfcls  17109  dfcon2  17161  llycmpkgen2  17261  trfil2  17598  fixufil  17633  tsmsres  17842  xrge0gsumle  18354  volsup  18929  mbfss  19017  itg2cnlem2  19133  iblss2  19176  vieta1lem2  19707  amgm  20301  wilthlem2  20323  ftalem3  20328  rpvmasum2  20677  iuninc  23174  rankaltopb  24585  hfun  24880  islimrs4  25685  comppfsc  26410  nacsfix  26890
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