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

Theorem ssundif 3876
Description: A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.)
Assertion
Ref Expression
ssundif  |-  ( A 
C_  ( B  u.  C )  <->  ( A  \  B )  C_  C
)

Proof of Theorem ssundif
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 pm5.6 920 . . . 4  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  ->  x  e.  C )  <->  ( x  e.  A  ->  ( x  e.  B  \/  x  e.  C ) ) )
2 eldif 3443 . . . . 5  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
32imbi1i 326 . . . 4  |-  ( ( x  e.  ( A 
\  B )  ->  x  e.  C )  <->  ( ( x  e.  A  /\  -.  x  e.  B
)  ->  x  e.  C ) )
4 elun 3603 . . . . 5  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
54imbi2i 313 . . . 4  |-  ( ( x  e.  A  ->  x  e.  ( B  u.  C ) )  <->  ( x  e.  A  ->  ( x  e.  B  \/  x  e.  C ) ) )
61, 3, 53bitr4ri 281 . . 3  |-  ( ( x  e.  A  ->  x  e.  ( B  u.  C ) )  <->  ( x  e.  ( A  \  B
)  ->  x  e.  C ) )
76albii 1687 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  ( B  u.  C
) )  <->  A. x
( x  e.  ( A  \  B )  ->  x  e.  C
) )
8 dfss2 3450 . 2  |-  ( A 
C_  ( B  u.  C )  <->  A. x
( x  e.  A  ->  x  e.  ( B  u.  C ) ) )
9 dfss2 3450 . 2  |-  ( ( A  \  B ) 
C_  C  <->  A. x
( x  e.  ( A  \  B )  ->  x  e.  C
) )
107, 8, 93bitr4i 280 1  |-  ( A 
C_  ( B  u.  C )  <->  ( A  \  B )  C_  C
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370   A.wal 1435    e. wcel 1867    \ cdif 3430    u. cun 3431    C_ wss 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447
This theorem is referenced by:  difcom  3877  uneqdifeq  3881  ssunsn2  4153  elpwun  6609  soex  6741  ressuppssdif  6938  frfi  7813  cantnfp1lem3  8175  dfacfin7  8818  zornn0g  8924  fpwwe2lem13  9056  hashbclem  12599  incexclem  13861  ramub1lem1  14936  lpcls  20304  cmpcld  20341  alexsubALTlem3  20988  restmetu  21509  uniiccdif  22429  abelthlem2  23278  abelthlem3  23279  imadifss  31661  frege124d  36025
  Copyright terms: Public domain W3C validator