Theorem unssbd 4122

Description: If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4118. Partial converse of unssd 4120. (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 4118	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
3	1, 2	sylibr 233	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simprd 496	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ∪ cun 3885   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904

This theorem is referenced by:  eldifpw  7618  ertr  8513  finsschain  9126  r0weon  9768  ackbij1lem16  9991  wunfi  10477  wunex2  10494  hashf1lem2  14170  sumsplit  15480  fsum2dlem  15482  fsumabs  15513  fsumrlim  15523  fsumo1  15524  fsumiun  15533  fprod2dlem  15690  mreexexlem3d  17355  yonedalem1  17990  yonedalem21  17991  yonedalem3a  17992  yonedalem4c  17995  yonedalem22  17996  yonedalem3b  17997  yonedainv  17999  yonffthlem  18000  ablfac1eulem  19675  lsmsp  20348  lsppratlem3  20411  mplcoe1  21238  mdetunilem9  21769  filufint  23071  fmfnfmlem4  23108  hausflim  23132  fclsfnflim  23178  fsumcn  24033  itgfsum  24991  jensenlem1  26136  jensenlem2  26137  gsumvsca1  31479  gsumvsca2  31480  ordtconnlem1  31874  vhmcls  33528  mclsppslem  33545  naddcllem  33831  rngunsnply  40998  brtrclfv2  41335