Theorem unssbd 4146

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3899   ⊆ wss 3901

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  eldifpw  7713  naddcllem  8604  ertr  8650  finsschain  9259  r0weon  9922  ackbij1lem16  10144  wunfi  10632  wunex2  10649  hashf1lem2  14379  sumsplit  15691  fsum2dlem  15693  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  fprod2dlem  15903  mreexexlem3d  17569  yonedalem1  18195  yonedalem21  18196  yonedalem3a  18197  yonedalem4c  18200  yonedalem22  18201  yonedalem3b  18202  yonedainv  18204  yonffthlem  18205  ablfac1eulem  20003  lsmsp  21038  lsppratlem3  21104  mplcoe1  21992  mdetunilem9  22564  filufint  23864  fmfnfmlem4  23901  hausflim  23925  fclsfnflim  23971  fsumcn  24817  itgfsum  25784  jensenlem1  26953  jensenlem2  26954  gsumvsca1  33308  gsumvsca2  33309  qsdrngilem  33575  evls1fldgencl  33827  fldextrspunlem1  33832  constrextdg2lem  33905  constrllcllem  33909  constrlccllem  33910  constrcccllem  33911  ordtconnlem1  34081  vhmcls  35760  mclsppslem  35777  rngunsnply  43411  brtrclfv2  43968