Theorem unssbd 4195

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154

This theorem is used by:  eldifpw  7814  naddcllem  8723  ertr  8771  finsschain  9386  r0weon  10130  ackbij1lem16  10351  wunfi  10845  wunex2  10862  hashf1lem2  14642  sumsplit  15978  fsum2dlem  15980  fsumabs  16012  fsumrlim  16022  fsumo1  16023  fsumiun  16032  fprod2dlem  16191  mreexexlem3d  17870  yonedalem1  18496  yonedalem21  18497  yonedalem3a  18498  yonedalem4c  18501  yonedalem22  18502  yonedalem3b  18503  yonedainv  18505  yonffthlem  18506  ablfac1eulem  20339  lsmsp  21412  lsppratlem3  21478  mplcoe1  22401  mdetunilem9  22990  filufint  24294  fmfnfmlem4  24331  hausflim  24355  fclsfnflim  24401  fsumcn  25246  itgfsum  26202  rngunsnply  26693  jensenlem1  27371  jensenlem2  27372  gsumvsca1  33886  gsumvsca2  33887  qsdrngilem  34122  evls1fldgencl  34413  fldextrspunlem1  34418  constrextdg2lem  34491  constrllcllem  34495  constrlccllem  34496  constrcccllem  34497  ordtconnlem1  34667  j0ltalephlem  36048  k2le  36063  vhmcls  36539  mclsppslem  36556  brtrclfv2  44988