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

Theorem ssequn1 3320
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
StepHypRef Expression
1 bicom 193 . . . 4  |-  ( ( x  e.  B  <->  ( x  e.  A  \/  x  e.  B ) )  <->  ( (
x  e.  A  \/  x  e.  B )  <->  x  e.  B ) )
2 pm4.72 851 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  B  <->  ( x  e.  A  \/  x  e.  B ) ) )
3 elun 3291 . . . . 5  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
43bibi1i 307 . . . 4  |-  ( ( x  e.  ( A  u.  B )  <->  x  e.  B )  <->  ( (
x  e.  A  \/  x  e.  B )  <->  x  e.  B ) )
51, 2, 43bitr4i 270 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  ( A  u.  B )  <->  x  e.  B ) )
65albii 1554 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x
( x  e.  ( A  u.  B )  <-> 
x  e.  B ) )
7 dfss2 3144 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
8 dfcleq 2252 . 2  |-  ( ( A  u.  B )  =  B  <->  A. x
( x  e.  ( A  u.  B )  <-> 
x  e.  B ) )
96, 7, 83bitr4i 270 1  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    \/ wo 359   A.wal 1532    = wceq 1619    e. wcel 1621    u. cun 3125    C_ wss 3127
This theorem is referenced by:  ssequn2  3323  undif  3509  uniop  4241  pwssun  4271  unisuc  4440  ordssun  4464  ordequn  4465  onun2i  4480  ordunpr  4589  onuninsuci  4603  funiunfv  5708  sorpssun  6218  domss2  6988  sucdom2  7025  findcard2s  7067  rankopb  7492  ranksuc  7505  kmlem11  7754  fin1a2lem10  8003  cvgcmpce  12242  mreexexlem3d  13511  dprd2da  15240  dpjcntz  15250  dpjdisj  15251  dpjlsm  15252  dpjidcl  15256  ablfac1eu  15271  perfcls  17056  dfcon2  17108  llycmpkgen2  17208  trfil2  17545  fixufil  17580  tsmsres  17789  xrge0gsumle  18301  volsup  18876  mbfss  18964  itg2cnlem2  19080  iblss2  19123  vieta1lem2  19654  amgm  20248  wilthlem2  20270  ftalem3  20275  rpvmasum2  20624  rankaltopb  23889  hfun  24184  islimrs4  24950  comppfsc  25675  nacsfix  26155
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-un 3132  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator