Theorem unssbd 4164

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

Syntax hints:   → wi 4   ∧ wa 398   ∪ cun 3934   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952

This theorem is referenced by:  eldifpw  7490  ertr  8304  finsschain  8831  r0weon  9438  ackbij1lem16  9657  wunfi  10143  wunex2  10160  hashf1lem2  13815  sumsplit  15123  fsum2dlem  15125  fsumabs  15156  fsumrlim  15166  fsumo1  15167  fsumiun  15176  fprod2dlem  15334  mreexexlem3d  16917  yonedalem1  17522  yonedalem21  17523  yonedalem3a  17524  yonedalem4c  17527  yonedalem22  17528  yonedalem3b  17529  yonedainv  17531  yonffthlem  17532  ablfac1eulem  19194  lsmsp  19858  lsppratlem3  19921  mplcoe1  20246  mdetunilem9  21229  filufint  22528  fmfnfmlem4  22565  hausflim  22589  fclsfnflim  22635  fsumcn  23478  itgfsum  24427  jensenlem1  25564  jensenlem2  25565  gsumvsca1  30854  gsumvsca2  30855  ordtconnlem1  31167  vhmcls  32813  mclsppslem  32830  rngunsnply  39793  brtrclfv2  40092