Theorem unssbd 4217

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3974   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  eldifpw  7803  naddcllem  8732  ertr  8778  finsschain  9429  r0weon  10081  ackbij1lem16  10303  wunfi  10790  wunex2  10807  hashf1lem2  14505  sumsplit  15816  fsum2dlem  15818  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  fprod2dlem  16028  mreexexlem3d  17704  yonedalem1  18342  yonedalem21  18343  yonedalem3a  18344  yonedalem4c  18347  yonedalem22  18348  yonedalem3b  18349  yonedainv  18351  yonffthlem  18352  ablfac1eulem  20116  lsmsp  21108  lsppratlem3  21174  mplcoe1  22078  mdetunilem9  22647  filufint  23949  fmfnfmlem4  23986  hausflim  24010  fclsfnflim  24056  fsumcn  24913  itgfsum  25882  jensenlem1  27048  jensenlem2  27049  gsumvsca1  33205  gsumvsca2  33206  qsdrngilem  33487  evls1fldgencl  33680  ordtconnlem1  33870  vhmcls  35534  mclsppslem  35551  rngunsnply  43130  brtrclfv2  43689