Theorem unssbd 4174

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3929   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948

This theorem is referenced by:  eldifpw  7767  naddcllem  8693  ertr  8739  finsschain  9376  r0weon  10031  ackbij1lem16  10253  wunfi  10740  wunex2  10757  hashf1lem2  14479  sumsplit  15789  fsum2dlem  15791  fsumabs  15822  fsumrlim  15832  fsumo1  15833  fsumiun  15842  fprod2dlem  16001  mreexexlem3d  17663  yonedalem1  18289  yonedalem21  18290  yonedalem3a  18291  yonedalem4c  18294  yonedalem22  18295  yonedalem3b  18296  yonedainv  18298  yonffthlem  18299  ablfac1eulem  20060  lsmsp  21049  lsppratlem3  21115  mplcoe1  22000  mdetunilem9  22563  filufint  23863  fmfnfmlem4  23900  hausflim  23924  fclsfnflim  23970  fsumcn  24817  itgfsum  25785  jensenlem1  26954  jensenlem2  26955  gsumvsca1  33228  gsumvsca2  33229  qsdrngilem  33514  evls1fldgencl  33716  fldextrspunlem1  33721  constrextdg2lem  33787  constrllcllem  33791  constrlccllem  33792  constrcccllem  33793  ordtconnlem1  33960  vhmcls  35593  mclsppslem  35610  rngunsnply  43160  brtrclfv2  43718