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

Theorem ssundif 3613
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 878 . . . 4  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  ->  x  e.  C )  <->  ( x  e.  A  ->  ( x  e.  B  \/  x  e.  C ) ) )
2 eldif 3238 . . . . 5  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
32imbi1i 315 . . . 4  |-  ( ( x  e.  ( A 
\  B )  ->  x  e.  C )  <->  ( ( x  e.  A  /\  -.  x  e.  B
)  ->  x  e.  C ) )
4 elun 3392 . . . . 5  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
54imbi2i 303 . . . 4  |-  ( ( x  e.  A  ->  x  e.  ( B  u.  C ) )  <->  ( x  e.  A  ->  ( x  e.  B  \/  x  e.  C ) ) )
61, 3, 53bitr4ri 269 . . 3  |-  ( ( x  e.  A  ->  x  e.  ( B  u.  C ) )  <->  ( x  e.  ( A  \  B
)  ->  x  e.  C ) )
76albii 1566 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  ( B  u.  C
) )  <->  A. x
( x  e.  ( A  \  B )  ->  x  e.  C
) )
8 dfss2 3245 . 2  |-  ( A 
C_  ( B  u.  C )  <->  A. x
( x  e.  A  ->  x  e.  ( B  u.  C ) ) )
9 dfss2 3245 . 2  |-  ( ( A  \  B ) 
C_  C  <->  A. x
( x  e.  ( A  \  B )  ->  x  e.  C
) )
107, 8, 93bitr4i 268 1  |-  ( A 
C_  ( B  u.  C )  <->  ( A  \  B )  C_  C
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358   A.wal 1540    e. wcel 1710    \ cdif 3225    u. cun 3226    C_ wss 3228
This theorem is referenced by:  difcom  3614  uneqdifeq  3618  ssunsn2  3852  elpwun  4646  soex  5201  frfi  7189  cantnfp1lem3  7469  dfacfin7  8112  zornn0g  8219  fpwwe2lem13  8351  hashbclem  11480  incexclem  12386  ramub1lem1  13164  lpcls  17192  cmpcld  17229  alexsubALTlem3  17839  uniiccdif  19031  abelthlem2  19909  abelthlem3  19910  restmetu  23615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator