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

Theorem ssequn1 3345
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 3316 . . . . 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 3169 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
8 dfcleq 2277 . 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 1684    u. cun 3150    C_ wss 3152
This theorem is referenced by:  ssequn2  3348  undif  3534  uniop  4269  pwssun  4299  unisuc  4468  ordssun  4492  ordequn  4493  onun2i  4508  ordunpr  4617  onuninsuci  4631  funiunfv  5774  sorpssun  6284  domss2  7020  sucdom2  7057  findcard2s  7099  rankopb  7524  ranksuc  7537  kmlem11  7786  fin1a2lem10  8035  cvgcmpce  12276  mreexexlem3d  13548  dprd2da  15277  dpjcntz  15287  dpjdisj  15288  dpjlsm  15289  dpjidcl  15293  ablfac1eu  15308  perfcls  17093  dfcon2  17145  llycmpkgen2  17245  trfil2  17582  fixufil  17617  tsmsres  17826  xrge0gsumle  18338  volsup  18913  mbfss  19001  itg2cnlem2  19117  iblss2  19160  vieta1lem2  19691  amgm  20285  wilthlem2  20307  ftalem3  20312  rpvmasum2  20661  iuninc  23158  rankaltopb  24513  hfun  24808  islimrs4  25582  comppfsc  26307  nacsfix  26787
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator