Theorem unssbd 4130

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

Syntax hints:   → wi 4   ∧ wa 396   ∪ cun 3888   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907

This theorem is referenced by:  eldifpw  7718  naddcllem  8609  ertr  8656  finsschain  9266  r0weon  9932  ackbij1lem16  10154  wunfi  10642  wunex2  10659  hashf1lem2  14416  sumsplit  15728  fsum2dlem  15730  fsumabs  15762  fsumrlim  15772  fsumo1  15773  fsumiun  15782  fprod2dlem  15943  mreexexlem3d  17610  yonedalem1  18236  yonedalem21  18237  yonedalem3a  18238  yonedalem4c  18241  yonedalem22  18242  yonedalem3b  18243  yonedainv  18245  yonffthlem  18246  ablfac1eulem  20047  lsmsp  21083  lsppratlem3  21149  mplcoe1  22020  mdetunilem9  22610  filufint  23910  fmfnfmlem4  23947  hausflim  23971  fclsfnflim  24017  fsumcn  24862  itgfsum  25819  jensenlem1  26975  jensenlem2  26976  gsumvsca1  33314  gsumvsca2  33315  qsdrngilem  33584  evls1fldgencl  33861  fldextrspunlem1  33866  constrextdg2lem  33939  constrllcllem  33943  constrlccllem  33944  constrcccllem  33945  ordtconnlem1  34115  vhmcls  35801  mclsppslem  35818  rngunsnply  43621  brtrclfv2  44178