Theorem unssbd 4148

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3901   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  eldifpw  7723  naddcllem  8614  ertr  8661  finsschain  9271  r0weon  9934  ackbij1lem16  10156  wunfi  10644  wunex2  10661  hashf1lem2  14391  sumsplit  15703  fsum2dlem  15705  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  fprod2dlem  15915  mreexexlem3d  17581  yonedalem1  18207  yonedalem21  18208  yonedalem3a  18209  yonedalem4c  18212  yonedalem22  18213  yonedalem3b  18214  yonedainv  18216  yonffthlem  18217  ablfac1eulem  20015  lsmsp  21050  lsppratlem3  21116  mplcoe1  22004  mdetunilem9  22576  filufint  23876  fmfnfmlem4  23913  hausflim  23937  fclsfnflim  23983  fsumcn  24829  itgfsum  25796  jensenlem1  26965  jensenlem2  26966  gsumvsca1  33319  gsumvsca2  33320  qsdrngilem  33586  evls1fldgencl  33847  fldextrspunlem1  33852  constrextdg2lem  33925  constrllcllem  33929  constrlccllem  33930  constrcccllem  33931  ordtconnlem1  34101  vhmcls  35779  mclsppslem  35796  rngunsnply  43523  brtrclfv2  44080