Theorem unssbd 4118

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  eldifpw  7596  ertr  8471  finsschain  9056  r0weon  9699  ackbij1lem16  9922  wunfi  10408  wunex2  10425  hashf1lem2  14098  sumsplit  15408  fsum2dlem  15410  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  fprod2dlem  15618  mreexexlem3d  17272  yonedalem1  17906  yonedalem21  17907  yonedalem3a  17908  yonedalem4c  17911  yonedalem22  17912  yonedalem3b  17913  yonedainv  17915  yonffthlem  17916  ablfac1eulem  19590  lsmsp  20263  lsppratlem3  20326  mplcoe1  21148  mdetunilem9  21677  filufint  22979  fmfnfmlem4  23016  hausflim  23040  fclsfnflim  23086  fsumcn  23939  itgfsum  24896  jensenlem1  26041  jensenlem2  26042  gsumvsca1  31381  gsumvsca2  31382  ordtconnlem1  31776  vhmcls  33428  mclsppslem  33445  naddcllem  33758  rngunsnply  40914  brtrclfv2  41224