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

Theorem ssequn1 3287
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 3258 . . . . 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 3111 . 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 3092    C_ wss 3094
This theorem is referenced by:  ssequn2  3290  undif  3476  uniop  4206  pwssun  4236  unisuc  4405  ordssun  4429  ordequn  4430  onun2i  4445  ordunpr  4554  onuninsuci  4568  funiunfv  5673  sorpssun  6183  domss2  6953  sucdom2  6990  findcard2s  7032  rankopb  7457  ranksuc  7470  kmlem11  7719  fin1a2lem10  7968  cvgcmpce  12206  mreexexlem3d  13475  dprd2da  15204  dpjcntz  15214  dpjdisj  15215  dpjlsm  15216  dpjidcl  15220  ablfac1eu  15235  perfcls  17020  dfcon2  17072  llycmpkgen2  17172  trfil2  17509  fixufil  17544  tsmsres  17753  xrge0gsumle  18265  volsup  18840  mbfss  18928  itg2cnlem2  19044  iblss2  19087  vieta1lem2  19618  amgm  20212  wilthlem2  20234  ftalem3  20239  rpvmasum2  20588  rankaltopb  23853  hfun  24148  islimrs4  24914  comppfsc  25639  nacsfix  26119
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 2742  df-un 3099  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator