Theorem unssbd 4155

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

Syntax hints:   → wi 4   ∧ wa 400   ∪ cun 3911   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930

This theorem is referenced by:  eldifpw  7763  naddcllem  8658  ertr  8706  finsschain  9312  r0weon  9992  ackbij1lem16  10213  wunfi  10702  wunex2  10719  hashf1lem2  14489  sumsplit  15815  fsum2dlem  15817  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  fprod2dlem  16030  mreexexlem3d  17698  yonedalem1  18324  yonedalem21  18325  yonedalem3a  18326  yonedalem4c  18329  yonedalem22  18330  yonedalem3b  18331  yonedainv  18333  yonffthlem  18334  ablfac1eulem  20140  lsmsp  21181  lsppratlem3  21247  mplcoe1  22153  mdetunilem9  22742  filufint  24042  fmfnfmlem4  24079  hausflim  24103  fclsfnflim  24149  fsumcn  24994  itgfsum  25951  jensenlem1  27113  jensenlem2  27114  gsumvsca1  33483  gsumvsca2  33484  qsdrngilem  33717  evls1fldgencl  34001  fldextrspunlem1  34006  constrextdg2lem  34079  constrllcllem  34083  constrlccllem  34084  constrcccllem  34085  ordtconnlem1  34255  vhmcls  35953  mclsppslem  35970  rngunsnply  43781  brtrclfv2  44338