Theorem unssbd 4135

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3888   ⊆ wss 3890

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 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  eldifpw  7715  naddcllem  8605  ertr  8652  finsschain  9262  r0weon  9925  ackbij1lem16  10147  wunfi  10635  wunex2  10652  hashf1lem2  14409  sumsplit  15721  fsum2dlem  15723  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  fprod2dlem  15936  mreexexlem3d  17603  yonedalem1  18229  yonedalem21  18230  yonedalem3a  18231  yonedalem4c  18234  yonedalem22  18235  yonedalem3b  18236  yonedainv  18238  yonffthlem  18239  ablfac1eulem  20040  lsmsp  21073  lsppratlem3  21139  mplcoe1  22025  mdetunilem9  22595  filufint  23895  fmfnfmlem4  23932  hausflim  23956  fclsfnflim  24002  fsumcn  24847  itgfsum  25804  jensenlem1  26964  jensenlem2  26965  gsumvsca1  33302  gsumvsca2  33303  qsdrngilem  33569  evls1fldgencl  33830  fldextrspunlem1  33835  constrextdg2lem  33908  constrllcllem  33912  constrlccllem  33913  constrcccllem  33914  ordtconnlem1  34084  vhmcls  35764  mclsppslem  35781  rngunsnply  43615  brtrclfv2  44172