Theorem ssundif 4493

Description: A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.)

Assertion

Ref	Expression
ssundif	⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶)

Proof of Theorem ssundif

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm5.6 1003	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
2		eldif 3972	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	2	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶))
4		elun 4162	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	4	imbi2i 336	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
6	1, 3, 5	3bitr4ri 304	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶))
7	6	albii 1815	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶))
8		df-ss 3979	. 2 ⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)))
9		df-ss 3979	. 2 ⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4i 303	1 ⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847  ∀wal 1534   ∈ wcel 2105   ∖ cdif 3959   ∪ cun 3960   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979

This theorem is referenced by:  difcom  4494  uneqdifeq  4498  ssunsn2  4831  elpwun  7787  soex  7943  ressuppssdif  8208  ssfi  9211  frfi  9318  cantnfp1lem3  9717  dfacfin7  10436  zornn0g  10542  fpwwe2lem12  10679  hashbclem  14487  incexclem  15868  ramub1lem1  17059  lpcls  23387  cmpcld  23425  alexsubALTlem3  24072  restmetu  24598  uniiccdif  25626  abelthlem2  26490  abelthlem3  26491  pmtrcnelor  33093  imadifss  37581  frege124d  43750