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

Theorem ssequn1 3347
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 3318 . . . . 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 1555 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x
( x  e.  ( A  u.  B )  <-> 
x  e.  B ) )
7 dfss2 3171 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
8 dfcleq 2279 . 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 1529    = wceq 1625    e. wcel 1686    u. cun 3152    C_ wss 3154
This theorem is referenced by:  ssequn2  3350  undif  3536  uniop  4271  pwssun  4301  unisuc  4470  ordssun  4494  ordequn  4495  onun2i  4510  ordunpr  4619  onuninsuci  4633  funiunfv  5776  sorpssun  6286  domss2  7022  sucdom2  7059  findcard2s  7101  rankopb  7526  ranksuc  7539  kmlem11  7788  fin1a2lem10  8037  cvgcmpce  12278  mreexexlem3d  13550  dprd2da  15279  dpjcntz  15289  dpjdisj  15290  dpjlsm  15291  dpjidcl  15295  ablfac1eu  15310  perfcls  17095  dfcon2  17147  llycmpkgen2  17247  trfil2  17584  fixufil  17619  tsmsres  17828  xrge0gsumle  18340  volsup  18915  mbfss  19003  itg2cnlem2  19119  iblss2  19162  vieta1lem2  19693  amgm  20287  wilthlem2  20309  ftalem3  20314  rpvmasum2  20663  iuninc  23160  rankaltopb  24515  hfun  24810  islimrs4  25593  comppfsc  26318  nacsfix  26798
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-un 3159  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator