Theorem unssbd 4157

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3912   ⊆ wss 3914

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 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  eldifpw  7744  naddcllem  8640  ertr  8686  finsschain  9310  r0weon  9965  ackbij1lem16  10187  wunfi  10674  wunex2  10691  hashf1lem2  14421  sumsplit  15734  fsum2dlem  15736  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  fprod2dlem  15946  mreexexlem3d  17607  yonedalem1  18233  yonedalem21  18234  yonedalem3a  18235  yonedalem4c  18238  yonedalem22  18239  yonedalem3b  18240  yonedainv  18242  yonffthlem  18243  ablfac1eulem  20004  lsmsp  20993  lsppratlem3  21059  mplcoe1  21944  mdetunilem9  22507  filufint  23807  fmfnfmlem4  23844  hausflim  23868  fclsfnflim  23914  fsumcn  24761  itgfsum  25728  jensenlem1  26897  jensenlem2  26898  gsumvsca1  33179  gsumvsca2  33180  qsdrngilem  33465  evls1fldgencl  33665  fldextrspunlem1  33670  constrextdg2lem  33738  constrllcllem  33742  constrlccllem  33743  constrcccllem  33744  ordtconnlem1  33914  vhmcls  35553  mclsppslem  35570  rngunsnply  43158  brtrclfv2  43716