Theorem unssbd 4147

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923

This theorem is used by:  eldifpw  7769  naddcllem  8664  ertr  8712  finsschain  9319  r0weon  10008  ackbij1lem16  10229  wunfi  10717  wunex2  10734  hashf1lem2  14506  sumsplit  15837  fsum2dlem  15839  fsumabs  15871  fsumrlim  15881  fsumo1  15882  fsumiun  15891  fprod2dlem  16052  mreexexlem3d  17719  yonedalem1  18345  yonedalem21  18346  yonedalem3a  18347  yonedalem4c  18350  yonedalem22  18351  yonedalem3b  18352  yonedainv  18354  yonffthlem  18355  ablfac1eulem  20167  lsmsp  21236  lsppratlem3  21302  mplcoe1  22217  mdetunilem9  22806  filufint  24106  fmfnfmlem4  24143  hausflim  24167  fclsfnflim  24213  fsumcn  25058  itgfsum  26015  jensenlem1  27180  jensenlem2  27181  gsumvsca1  33569  gsumvsca2  33570  qsdrngilem  33799  evls1fldgencl  34083  fldextrspunlem1  34088  constrextdg2lem  34161  constrllcllem  34165  constrlccllem  34166  constrcccllem  34167  ordtconnlem1  34337  vhmcls  36071  mclsppslem  36088  rngunsnply  43929  brtrclfv2  44486