Theorem ssundif 4442

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 1017	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
2		eldif 4049	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	2	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶))
4		elun 4152	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	4	imbi2i 339	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
6	1, 3, 5	3bitr4ri 307	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶))
7	6	albii 1851	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶))
8		df-ss 3896	. 2 ⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)))
9		df-ss 3896	. 2 ⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶))
10	7, 8, 9	3bitr4i 306	1 ⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∀wal 1567   ∈ wcel 2144   ⊆ wss 3895   ∖ cdif 4045   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151

This theorem is used by:  difcom  4443  uneqdifeq  4447  ssunsn2  4782  imadifssrn  6201  elpwun  7784  soex  7934  ressuppssdif  8206  ssfi  9192  frfi  9280  cantnfp1lem3  9685  dfacfin7  10481  zornn0g  10587  fpwwe2lem12  10731  hashbclem  14601  incexclem  16011  ramub1lem1  17210  lpcls  23688  cmpcld  23726  alexsubALTlem3  24374  restmetu  24895  uniiccdif  25905  abelthlem2  26765  abelthlem3  26766  pmtrcnelor  33699  imadifss  38617  frege124d  44855