Theorem unssbd 4192

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3895   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151

This theorem is used by:  eldifpw  7783  naddcllem  8689  ertr  8737  finsschain  9352  r0weon  10095  ackbij1lem16  10316  wunfi  10810  wunex2  10827  hashf1lem2  14605  sumsplit  15940  fsum2dlem  15942  fsumabs  15974  fsumrlim  15984  fsumo1  15985  fsumiun  15994  fprod2dlem  16153  mreexexlem3d  17826  yonedalem1  18452  yonedalem21  18453  yonedalem3a  18454  yonedalem4c  18457  yonedalem22  18458  yonedalem3b  18459  yonedainv  18461  yonffthlem  18462  ablfac1eulem  20294  lsmsp  21367  lsppratlem3  21433  mplcoe1  22352  mdetunilem9  22941  filufint  24245  fmfnfmlem4  24282  hausflim  24306  fclsfnflim  24352  fsumcn  25197  itgfsum  26153  jensenlem1  27320  jensenlem2  27321  gsumvsca1  33834  gsumvsca2  33835  qsdrngilem  34065  evls1fldgencl  34349  fldextrspunlem1  34354  constrextdg2lem  34427  constrllcllem  34431  constrlccllem  34432  constrcccllem  34433  ordtconnlem1  34603  j0ltalephlem  35947  vhmcls  36418  mclsppslem  36435  rngunsnply  44265  brtrclfv2  44821