Theorem unssbd 4204

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3961   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980

This theorem is referenced by:  eldifpw  7787  naddcllem  8713  ertr  8759  finsschain  9397  r0weon  10050  ackbij1lem16  10272  wunfi  10759  wunex2  10776  hashf1lem2  14492  sumsplit  15801  fsum2dlem  15803  fsumabs  15834  fsumrlim  15844  fsumo1  15845  fsumiun  15854  fprod2dlem  16013  mreexexlem3d  17691  yonedalem1  18329  yonedalem21  18330  yonedalem3a  18331  yonedalem4c  18334  yonedalem22  18335  yonedalem3b  18336  yonedainv  18338  yonffthlem  18339  ablfac1eulem  20107  lsmsp  21103  lsppratlem3  21169  mplcoe1  22073  mdetunilem9  22642  filufint  23944  fmfnfmlem4  23981  hausflim  24005  fclsfnflim  24051  fsumcn  24908  itgfsum  25877  jensenlem1  27045  jensenlem2  27046  gsumvsca1  33215  gsumvsca2  33216  qsdrngilem  33502  evls1fldgencl  33695  ordtconnlem1  33885  vhmcls  35551  mclsppslem  35568  rngunsnply  43158  brtrclfv2  43717