Theorem ssundif 3767

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 903	. . . 4 |- ( ( ( x e. A /\ -. x e. B ) -> x e. C ) <-> ( x e. A -> ( x e. B \/ x e. C ) ) )
2		eldif 3343	. . . . 5 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	2	imbi1i 325	. . . 4 |- ( ( x e. ( A \ B ) -> x e. C ) <-> ( ( x e. A /\ -. x e. B ) -> x e. C ) )
4		elun 3502	. . . . 5 |- ( x e. ( B u. C ) <-> ( x e. B \/ x e. C ) )
5	4	imbi2i 312	. . . 4 |- ( ( x e. A -> x e. ( B u. C ) ) <-> ( x e. A -> ( x e. B \/ x e. C ) ) )
6	1, 3, 5	3bitr4ri 278	. . 3 |- ( ( x e. A -> x e. ( B u. C ) ) <-> ( x e. ( A \ B ) -> x e. C ) )
7	6	albii 1610	. 2 |- ( A. x ( x e. A -> x e. ( B u. C ) ) <-> A. x ( x e. ( A \ B ) -> x e. C ) )
8		dfss2 3350	. 2 |- ( A C_ ( B u. C ) <-> A. x ( x e. A -> x e. ( B u. C ) ) )
9		dfss2 3350	. 2 |- ( ( A \ B ) C_ C <-> A. x ( x e. ( A \ B ) -> x e. C ) )
10	7, 8, 9	3bitr4i 277	1 |- ( A C_ ( B u. C ) <-> ( A \ B ) C_ C )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   A.wal 1367   e. wcel 1756   \ cdif 3330   u. cun 3331   C_ wss 3333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347

This theorem is referenced by:  difcom  3768  uneqdifeq  3772  ssunsn2  4037  elpwun  6394  soex  6526  ressuppssdif  6715  frfi  7562  cantnfp1lem3  7893  cantnfp1lem3OLD  7919  dfacfin7  8573  zornn0g  8679  fpwwe2lem13  8814  hashbclem  12210  incexclem  13304  ramub1lem1  14092  lpcls  18973  cmpcld  19010  alexsubALTlem3  19626  restmetu  20167  uniiccdif  21063  abelthlem2  21902  abelthlem3  21903