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

Theorem ssundif 3537
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 3162 . . . . 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 3316 . . . . 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 1553 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  ( B  u.  C
) )  <->  A. x
( x  e.  ( A  \  B )  ->  x  e.  C
) )
8 dfss2 3169 . 2  |-  ( A 
C_  ( B  u.  C )  <->  A. x
( x  e.  A  ->  x  e.  ( B  u.  C ) ) )
9 dfss2 3169 . 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 1527    e. wcel 1684    \ cdif 3149    u. cun 3150    C_ wss 3152
This theorem is referenced by:  difcom  3538  uneqdifeq  3542  ssunsn2  3773  elpwun  4567  soex  5122  frfi  7102  cantnfp1lem3  7382  dfacfin7  8025  zornn0g  8132  fpwwe2lem13  8264  hashbclem  11390  incexclem  12295  ramub1lem1  13073  lpcls  17092  cmpcld  17129  alexsubALTlem3  17743  uniiccdif  18933  abelthlem2  19808  abelthlem3  19809  sssu  25141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator