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

Theorem ssequn1 3346
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 191 . . . 4  |-  ( ( x  e.  B  <->  ( x  e.  A  \/  x  e.  B ) )  <->  ( (
x  e.  A  \/  x  e.  B )  <->  x  e.  B ) )
2 pm4.72 846 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  B  <->  ( x  e.  A  \/  x  e.  B ) ) )
3 elun 3317 . . . . 5  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
43bibi1i 305 . . . 4  |-  ( ( x  e.  ( A  u.  B )  <->  x  e.  B )  <->  ( (
x  e.  A  \/  x  e.  B )  <->  x  e.  B ) )
51, 2, 43bitr4i 268 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  ( A  u.  B )  <->  x  e.  B ) )
65albii 1553 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x
( x  e.  ( A  u.  B )  <-> 
x  e.  B ) )
7 dfss2 3170 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
8 dfcleq 2278 . 2  |-  ( ( A  u.  B )  =  B  <->  A. x
( x  e.  ( A  u.  B )  <-> 
x  e.  B ) )
96, 7, 83bitr4i 268 1  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357   A.wal 1527    = wceq 1623    e. wcel 1685    u. cun 3151    C_ wss 3153
This theorem is referenced by:  ssequn2  3349  undif  3535  uniop  4268  pwssun  4298  unisuc  4467  ordssun  4491  ordequn  4492  onun2i  4507  ordunpr  4616  onuninsuci  4630  funiunfv  5736  sorpssun  6246  domss2  7016  sucdom2  7053  findcard2s  7095  rankopb  7520  ranksuc  7533  kmlem11  7782  fin1a2lem10  8031  cvgcmpce  12272  mreexexlem3d  13544  dprd2da  15273  dpjcntz  15283  dpjdisj  15284  dpjlsm  15285  dpjidcl  15289  ablfac1eu  15304  perfcls  17089  dfcon2  17141  llycmpkgen2  17241  trfil2  17578  fixufil  17613  tsmsres  17822  xrge0gsumle  18334  volsup  18909  mbfss  18997  itg2cnlem2  19113  iblss2  19156  vieta1lem2  19687  amgm  20281  wilthlem2  20303  ftalem3  20308  rpvmasum2  20657  rankaltopb  23923  hfun  24218  islimrs4  24993  comppfsc  25718  nacsfix  26198
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator