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

Theorem ssequn1 3453
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 192 . . . 4  |-  ( ( x  e.  B  <->  ( x  e.  A  \/  x  e.  B ) )  <->  ( (
x  e.  A  \/  x  e.  B )  <->  x  e.  B ) )
2 pm4.72 847 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  B  <->  ( x  e.  A  \/  x  e.  B ) ) )
3 elun 3424 . . . . 5  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
43bibi1i 306 . . . 4  |-  ( ( x  e.  ( A  u.  B )  <->  x  e.  B )  <->  ( (
x  e.  A  \/  x  e.  B )  <->  x  e.  B ) )
51, 2, 43bitr4i 269 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  ( A  u.  B )  <->  x  e.  B ) )
65albii 1572 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x
( x  e.  ( A  u.  B )  <-> 
x  e.  B ) )
7 dfss2 3273 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
8 dfcleq 2374 . 2  |-  ( ( A  u.  B )  =  B  <->  A. x
( x  e.  ( A  u.  B )  <-> 
x  e.  B ) )
96, 7, 83bitr4i 269 1  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358   A.wal 1546    = wceq 1649    e. wcel 1717    u. cun 3254    C_ wss 3256
This theorem is referenced by:  ssequn2  3456  undif  3644  uniop  4393  pwssun  4423  unisuc  4591  ordssun  4614  ordequn  4615  onun2i  4630  ordunpr  4739  onuninsuci  4753  funiunfv  5927  sorpssun  6458  domss2  7195  sucdom2  7232  findcard2s  7278  rankopb  7704  ranksuc  7717  kmlem11  7966  fin1a2lem10  8215  cvgcmpce  12517  mreexexlem3d  13791  dprd2da  15520  dpjcntz  15530  dpjdisj  15531  dpjlsm  15532  dpjidcl  15536  ablfac1eu  15551  perfcls  17344  dfcon2  17396  llycmpkgen2  17496  trfil2  17833  fixufil  17868  tsmsres  18087  ustssco  18158  ustuqtop1  18185  xrge0gsumle  18728  volsup  19310  mbfss  19398  itg2cnlem2  19514  iblss2  19557  vieta1lem2  20088  amgm  20689  wilthlem2  20712  ftalem3  20717  rpvmasum2  21066  iuninc  23848  rankaltopb  25531  hfun  25826  comppfsc  26071  nacsfix  26450
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-un 3261  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator