Theorem unssbd 4153

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

Syntax hints:   → wi 4   ∧ wa 396   ∪ cun 3911   ⊆ wss 3913

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918  df-in 3920  df-ss 3930

This theorem is referenced by:  eldifpw  7707  naddcllem  8627  ertr  8670  finsschain  9310  r0weon  9957  ackbij1lem16  10180  wunfi  10666  wunex2  10683  hashf1lem2  14367  sumsplit  15664  fsum2dlem  15666  fsumabs  15697  fsumrlim  15707  fsumo1  15708  fsumiun  15717  fprod2dlem  15874  mreexexlem3d  17540  yonedalem1  18175  yonedalem21  18176  yonedalem3a  18177  yonedalem4c  18180  yonedalem22  18181  yonedalem3b  18182  yonedainv  18184  yonffthlem  18185  ablfac1eulem  19865  lsmsp  20604  lsppratlem3  20669  mplcoe1  21475  mdetunilem9  22006  filufint  23308  fmfnfmlem4  23345  hausflim  23369  fclsfnflim  23415  fsumcn  24270  itgfsum  25228  jensenlem1  26373  jensenlem2  26374  gsumvsca1  32131  gsumvsca2  32132  ordtconnlem1  32594  vhmcls  34247  mclsppslem  34264  rngunsnply  41558  brtrclfv2  42121