Theorem unssbd 4143

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3896   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915

This theorem is referenced by:  eldifpw  7709  naddcllem  8599  ertr  8645  finsschain  9252  r0weon  9912  ackbij1lem16  10134  wunfi  10621  wunex2  10638  hashf1lem2  14367  sumsplit  15679  fsum2dlem  15681  fsumabs  15712  fsumrlim  15722  fsumo1  15723  fsumiun  15732  fprod2dlem  15891  mreexexlem3d  17556  yonedalem1  18182  yonedalem21  18183  yonedalem3a  18184  yonedalem4c  18187  yonedalem22  18188  yonedalem3b  18189  yonedainv  18191  yonffthlem  18192  ablfac1eulem  19990  lsmsp  21024  lsppratlem3  21090  mplcoe1  21975  mdetunilem9  22538  filufint  23838  fmfnfmlem4  23875  hausflim  23899  fclsfnflim  23945  fsumcn  24791  itgfsum  25758  jensenlem1  26927  jensenlem2  26928  gsumvsca1  33204  gsumvsca2  33205  qsdrngilem  33468  evls1fldgencl  33706  fldextrspunlem1  33711  constrextdg2lem  33784  constrllcllem  33788  constrlccllem  33789  constrcccllem  33790  ordtconnlem1  33960  vhmcls  35633  mclsppslem  35650  rngunsnply  43289  brtrclfv2  43847