Theorem unssbd 4115

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

Syntax hints:   → wi 4   ∧ wa 399   ∪ cun 3879   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898

This theorem is referenced by:  eldifpw  7470  ertr  8287  finsschain  8815  r0weon  9423  ackbij1lem16  9646  wunfi  10132  wunex2  10149  hashf1lem2  13810  sumsplit  15115  fsum2dlem  15117  fsumabs  15148  fsumrlim  15158  fsumo1  15159  fsumiun  15168  fprod2dlem  15326  mreexexlem3d  16909  yonedalem1  17514  yonedalem21  17515  yonedalem3a  17516  yonedalem4c  17519  yonedalem22  17520  yonedalem3b  17521  yonedainv  17523  yonffthlem  17524  ablfac1eulem  19187  lsmsp  19851  lsppratlem3  19914  mplcoe1  20705  mdetunilem9  21225  filufint  22525  fmfnfmlem4  22562  hausflim  22586  fclsfnflim  22632  fsumcn  23475  itgfsum  24430  jensenlem1  25572  jensenlem2  25573  gsumvsca1  30904  gsumvsca2  30905  ordtconnlem1  31277  vhmcls  32926  mclsppslem  32943  rngunsnply  40117  brtrclfv2  40428