Theorem unssbd 3753

Description: If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 3749. Partial converse of unssd 3751. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
unssad.1	⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)

Assertion

Ref	Expression
unssbd	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem unssbd

Step	Hyp	Ref	Expression
1		unssad.1	. . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
2		unss 3749	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
3	1, 2	sylibr 223	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simprd 478	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 383   ∪ cun 3538   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554

This theorem is referenced by:  eldifpw  6868  ertr  7644  finsschain  8156  r0weon  8718  ackbij1lem16  8940  wunfi  9422  wunex2  9439  hashf1lem2  13097  sumsplit  14341  fsum2dlem  14343  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  fprod2dlem  14549  mreexexlem3d  16129  yonedalem1  16735  yonedalem21  16736  yonedalem3a  16737  yonedalem4c  16740  yonedalem22  16741  yonedalem3b  16742  yonedainv  16744  yonffthlem  16745  ablfac1eulem  18294  lsmsp  18907  lsppratlem3  18970  mplcoe1  19286  mdetunilem9  20245  filufint  21534  fmfnfmlem4  21571  hausflim  21595  fclsfnflim  21641  fsumcn  22481  mbfeqalem  23215  itgfsum  23399  jensenlem1  24513  jensenlem2  24514  gsumvsca1  29113  gsumvsca2  29114  ordtconlem1  29298  vhmcls  30717  mclsppslem  30734  rngunsnply  36762  brtrclfv2  37038