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

Theorem ssequn1 3306
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 3277 . . . . 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 3130 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
8 dfcleq 2250 . 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 3111    C_ wss 3113
This theorem is referenced by:  ssequn2  3309  undif  3495  uniop  4227  pwssun  4257  unisuc  4426  ordssun  4450  ordequn  4451  onun2i  4466  ordunpr  4575  onuninsuci  4589  funiunfv  5694  sorpssun  6204  domss2  6974  sucdom2  7011  findcard2s  7053  rankopb  7478  ranksuc  7491  kmlem11  7740  fin1a2lem10  7989  cvgcmpce  12227  mreexexlem3d  13496  dprd2da  15225  dpjcntz  15235  dpjdisj  15236  dpjlsm  15237  dpjidcl  15241  ablfac1eu  15256  perfcls  17041  dfcon2  17093  llycmpkgen2  17193  trfil2  17530  fixufil  17565  tsmsres  17774  xrge0gsumle  18286  volsup  18861  mbfss  18949  itg2cnlem2  19065  iblss2  19108  vieta1lem2  19639  amgm  20233  wilthlem2  20255  ftalem3  20260  rpvmasum2  20609  rankaltopb  23874  hfun  24169  islimrs4  24935  comppfsc  25660  nacsfix  26140
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-un 3118  df-in 3120  df-ss 3127
  Copyright terms: Public domain W3C validator