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

Theorem ssundif 3853
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 924 . . . 4  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  ->  x  e.  C )  <->  ( x  e.  A  ->  ( x  e.  B  \/  x  e.  C ) ) )
2 eldif 3416 . . . . 5  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
32imbi1i 327 . . . 4  |-  ( ( x  e.  ( A 
\  B )  ->  x  e.  C )  <->  ( ( x  e.  A  /\  -.  x  e.  B
)  ->  x  e.  C ) )
4 elun 3576 . . . . 5  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
54imbi2i 314 . . . 4  |-  ( ( x  e.  A  ->  x  e.  ( B  u.  C ) )  <->  ( x  e.  A  ->  ( x  e.  B  \/  x  e.  C ) ) )
61, 3, 53bitr4ri 282 . . 3  |-  ( ( x  e.  A  ->  x  e.  ( B  u.  C ) )  <->  ( x  e.  ( A  \  B
)  ->  x  e.  C ) )
76albii 1693 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  ( B  u.  C
) )  <->  A. x
( x  e.  ( A  \  B )  ->  x  e.  C
) )
8 dfss2 3423 . 2  |-  ( A 
C_  ( B  u.  C )  <->  A. x
( x  e.  A  ->  x  e.  ( B  u.  C ) ) )
9 dfss2 3423 . 2  |-  ( ( A  \  B ) 
C_  C  <->  A. x
( x  e.  ( A  \  B )  ->  x  e.  C
) )
107, 8, 93bitr4i 281 1  |-  ( A 
C_  ( B  u.  C )  <->  ( A  \  B )  C_  C
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    \/ wo 370    /\ wa 371   A.wal 1444    e. wcel 1889    \ cdif 3403    u. cun 3404    C_ wss 3406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420
This theorem is referenced by:  difcom  3854  uneqdifeq  3858  ssunsn2  4134  elpwun  6609  soex  6741  ressuppssdif  6941  frfi  7821  cantnfp1lem3  8190  dfacfin7  8834  zornn0g  8940  fpwwe2lem13  9072  hashbclem  12622  incexclem  13906  ramub1lem1  14996  lpcls  20392  cmpcld  20429  alexsubALTlem3  21076  restmetu  21597  uniiccdif  22547  abelthlem2  23399  abelthlem3  23400  imadifss  31940  frege124d  36365
  Copyright terms: Public domain W3C validator