Theorem unssbd 4144

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

Syntax hints:   → wi 4   ∧ wa 399   ∪ cun 3900   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-ss 3919

This theorem is referenced by:  eldifpw  7745  naddcllem  8639  ertr  8687  finsschain  9295  r0weon  9961  ackbij1lem16  10183  wunfi  10672  wunex2  10689  hashf1lem2  14462  sumsplit  15785  fsum2dlem  15787  fsumabs  15819  fsumrlim  15829  fsumo1  15830  fsumiun  15839  fprod2dlem  16000  mreexexlem3d  17668  yonedalem1  18294  yonedalem21  18295  yonedalem3a  18296  yonedalem4c  18299  yonedalem22  18300  yonedalem3b  18301  yonedainv  18303  yonffthlem  18304  ablfac1eulem  20104  lsmsp  21140  lsppratlem3  21206  mplcoe1  22077  mdetunilem9  22667  filufint  23967  fmfnfmlem4  24004  hausflim  24028  fclsfnflim  24074  fsumcn  24919  itgfsum  25876  jensenlem1  27038  jensenlem2  27039  gsumvsca1  33366  gsumvsca2  33367  qsdrngilem  33642  evls1fldgencl  33927  fldextrspunlem1  33932  constrextdg2lem  34005  constrllcllem  34009  constrlccllem  34010  constrcccllem  34011  ordtconnlem1  34181  vhmcls  35876  mclsppslem  35893  rngunsnply  43706  brtrclfv2  44263