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

Theorem ssequn1 3485
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 3456 . . . . 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 3305 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
8 dfcleq 2406 . 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 1721    u. cun 3286    C_ wss 3288
This theorem is referenced by:  ssequn2  3488  undif  3676  uniop  4427  pwssun  4457  unisuc  4625  ordssun  4648  ordequn  4649  onun2i  4664  ordunpr  4773  onuninsuci  4787  funiunfv  5962  sorpssun  6496  domss2  7233  sucdom2  7270  findcard2s  7316  rankopb  7742  ranksuc  7755  kmlem11  8004  fin1a2lem10  8253  cvgcmpce  12560  mreexexlem3d  13834  dprd2da  15563  dpjcntz  15573  dpjdisj  15574  dpjlsm  15575  dpjidcl  15579  ablfac1eu  15594  perfcls  17391  dfcon2  17443  llycmpkgen2  17543  trfil2  17880  fixufil  17915  tsmsres  18134  ustssco  18205  ustuqtop1  18232  xrge0gsumle  18825  volsup  19411  mbfss  19499  itg2cnlem2  19615  iblss2  19658  vieta1lem2  20189  amgm  20790  wilthlem2  20813  ftalem3  20818  rpvmasum2  21167  iuninc  23972  rankaltopb  25736  hfun  26031  comppfsc  26285  nacsfix  26664
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
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 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-un 3293  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator