Theorem ssundif 3876

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 920	. . . 4 |- ( ( ( x e. A /\ -. x e. B ) -> x e. C ) <-> ( x e. A -> ( x e. B \/ x e. C ) ) )
2		eldif 3443	. . . . 5 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	2	imbi1i 326	. . . 4 |- ( ( x e. ( A \ B ) -> x e. C ) <-> ( ( x e. A /\ -. x e. B ) -> x e. C ) )
4		elun 3603	. . . . 5 |- ( x e. ( B u. C ) <-> ( x e. B \/ x e. C ) )
5	4	imbi2i 313	. . . 4 |- ( ( x e. A -> x e. ( B u. C ) ) <-> ( x e. A -> ( x e. B \/ x e. C ) ) )
6	1, 3, 5	3bitr4ri 281	. . 3 |- ( ( x e. A -> x e. ( B u. C ) ) <-> ( x e. ( A \ B ) -> x e. C ) )
7	6	albii 1687	. 2 |- ( A. x ( x e. A -> x e. ( B u. C ) ) <-> A. x ( x e. ( A \ B ) -> x e. C ) )
8		dfss2 3450	. 2 |- ( A C_ ( B u. C ) <-> A. x ( x e. A -> x e. ( B u. C ) ) )
9		dfss2 3450	. 2 |- ( ( A \ B ) C_ C <-> A. x ( x e. ( A \ B ) -> x e. C ) )
10	7, 8, 9	3bitr4i 280	1 |- ( A C_ ( B u. C ) <-> ( A \ B ) C_ C )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   A.wal 1435   e. wcel 1867   \ cdif 3430   u. cun 3431   C_ wss 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447

This theorem is referenced by:  difcom  3877  uneqdifeq  3881  ssunsn2  4153  elpwun  6609  soex  6741  ressuppssdif  6938  frfi  7813  cantnfp1lem3  8175  dfacfin7  8818  zornn0g  8924  fpwwe2lem13  9056  hashbclem  12599  incexclem  13861  ramub1lem1  14936  lpcls  20304  cmpcld  20341  alexsubALTlem3  20988  restmetu  21509  uniiccdif  22429  abelthlem2  23278  abelthlem3  23279  imadifss  31661  frege124d  36025