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

Theorem ssundif 3735
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 880 . . . 4  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  ->  x  e.  C )  <->  ( x  e.  A  ->  ( x  e.  B  \/  x  e.  C ) ) )
2 eldif 3316 . . . . 5  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
32imbi1i 317 . . . 4  |-  ( ( x  e.  ( A 
\  B )  ->  x  e.  C )  <->  ( ( x  e.  A  /\  -.  x  e.  B
)  ->  x  e.  C ) )
4 elun 3474 . . . . 5  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
54imbi2i 305 . . . 4  |-  ( ( x  e.  A  ->  x  e.  ( B  u.  C ) )  <->  ( x  e.  A  ->  ( x  e.  B  \/  x  e.  C ) ) )
61, 3, 53bitr4ri 271 . . 3  |-  ( ( x  e.  A  ->  x  e.  ( B  u.  C ) )  <->  ( x  e.  ( A  \  B
)  ->  x  e.  C ) )
76albii 1576 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  ( B  u.  C
) )  <->  A. x
( x  e.  ( A  \  B )  ->  x  e.  C
) )
8 dfss2 3323 . 2  |-  ( A 
C_  ( B  u.  C )  <->  A. x
( x  e.  A  ->  x  e.  ( B  u.  C ) ) )
9 dfss2 3323 . 2  |-  ( ( A  \  B ) 
C_  C  <->  A. x
( x  e.  ( A  \  B )  ->  x  e.  C
) )
107, 8, 93bitr4i 270 1  |-  ( A 
C_  ( B  u.  C )  <->  ( A  \  B )  C_  C
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360   A.wal 1550    e. wcel 1727    \ cdif 3303    u. cun 3304    C_ wss 3306
This theorem is referenced by:  difcom  3736  uneqdifeq  3740  ssunsn2  3982  elpwun  4785  soex  5348  frfi  7381  cantnfp1lem3  7665  dfacfin7  8310  zornn0g  8416  fpwwe2lem13  8548  hashbclem  11732  incexclem  12647  ramub1lem1  13425  lpcls  17459  cmpcld  17496  alexsubALTlem3  18111  restmetu  18648  uniiccdif  19501  abelthlem2  20379  abelthlem3  20380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320
  Copyright terms: Public domain W3C validator