Theorem unssbd 4147

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3903   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922

This theorem is referenced by:  eldifpw  7708  naddcllem  8601  ertr  8647  finsschain  9268  r0weon  9925  ackbij1lem16  10147  wunfi  10634  wunex2  10651  hashf1lem2  14381  sumsplit  15693  fsum2dlem  15695  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  fprod2dlem  15905  mreexexlem3d  17570  yonedalem1  18196  yonedalem21  18197  yonedalem3a  18198  yonedalem4c  18201  yonedalem22  18202  yonedalem3b  18203  yonedainv  18205  yonffthlem  18206  ablfac1eulem  19971  lsmsp  21008  lsppratlem3  21074  mplcoe1  21960  mdetunilem9  22523  filufint  23823  fmfnfmlem4  23860  hausflim  23884  fclsfnflim  23930  fsumcn  24777  itgfsum  25744  jensenlem1  26913  jensenlem2  26914  gsumvsca1  33181  gsumvsca2  33182  qsdrngilem  33444  evls1fldgencl  33644  fldextrspunlem1  33649  constrextdg2lem  33717  constrllcllem  33721  constrlccllem  33722  constrcccllem  33723  ordtconnlem1  33893  vhmcls  35541  mclsppslem  35558  rngunsnply  43145  brtrclfv2  43703