Theorem unssbd 4134

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3887   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906

This theorem is referenced by:  eldifpw  7722  naddcllem  8612  ertr  8659  finsschain  9269  r0weon  9934  ackbij1lem16  10156  wunfi  10644  wunex2  10661  hashf1lem2  14418  sumsplit  15730  fsum2dlem  15732  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  fprod2dlem  15945  mreexexlem3d  17612  yonedalem1  18238  yonedalem21  18239  yonedalem3a  18240  yonedalem4c  18243  yonedalem22  18244  yonedalem3b  18245  yonedainv  18247  yonffthlem  18248  ablfac1eulem  20049  lsmsp  21081  lsppratlem3  21147  mplcoe1  22015  mdetunilem9  22585  filufint  23885  fmfnfmlem4  23922  hausflim  23946  fclsfnflim  23992  fsumcn  24837  itgfsum  25794  jensenlem1  26950  jensenlem2  26951  gsumvsca1  33287  gsumvsca2  33288  qsdrngilem  33554  evls1fldgencl  33814  fldextrspunlem1  33819  constrextdg2lem  33892  constrllcllem  33896  constrlccllem  33897  constrcccllem  33898  ordtconnlem1  34068  vhmcls  35748  mclsppslem  35765  rngunsnply  43597  brtrclfv2  44154