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

Theorem ssequn1 3255
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 3226 . . . . 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 3092 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
8 dfcleq 2247 . 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 3076    C_ wss 3078
This theorem is referenced by:  ssequn2  3258  undif  3440  uniop  4162  pwssun  4192  unisuc  4361  ordssun  4383  ordequn  4384  onun2i  4399  ordunpr  4508  onuninsuci  4522  funiunfv  5626  sorpssun  6136  domss2  6905  sucdom2  6942  findcard2s  6984  rankopb  7408  ranksuc  7421  kmlem11  7670  fin1a2lem10  7919  cvgcmpce  12153  dprd2da  15112  dpjcntz  15122  dpjdisj  15123  dpjlsm  15124  dpjidcl  15128  ablfac1eu  15143  perfcls  16925  dfcon2  16977  llycmpkgen2  17077  trfil2  17414  fixufil  17449  tsmsres  17658  xrge0gsumle  18170  volsup  18745  mbfss  18833  itg2cnlem2  18949  iblss2  18992  vieta1lem2  19523  amgm  20117  wilthlem2  20139  ftalem3  20144  rpvmasum2  20493  rankaltopb  23687  hfun  23982  islimrs4  24748  comppfsc  25473  nacsfix  25953
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator