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.

Step	Hyp	Ref	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 ) )
3	2	imbi1i 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 ) )
5	4	imbi2i 314	. . . 4 |- ( ( x e. A -> x e. ( B u. C ) ) <-> ( x e. A -> ( x e. B \/ x e. C ) ) )
6	1, 3, 5	3bitr4ri 282	. . 3 |- ( ( x e. A -> x e. ( B u. C ) ) <-> ( x e. ( A \ B ) -> x e. C ) )
7	6	albii 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 ) )
10	7, 8, 9	3bitr4i 281	1 |- ( A C_ ( B u. C ) <-> ( A \ B ) C_ C )

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