Theorem unssbd 3791

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

Syntax hints:   → wi 4   ∧ wa 384   ∪ cun 3572   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588

This theorem is referenced by:  eldifpw  6976  ertr  7757  finsschain  8273  r0weon  8835  ackbij1lem16  9057  wunfi  9543  wunex2  9560  hashf1lem2  13240  sumsplit  14499  fsum2dlem  14501  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  fprod2dlem  14710  mreexexlem3d  16306  yonedalem1  16912  yonedalem21  16913  yonedalem3a  16914  yonedalem4c  16917  yonedalem22  16918  yonedalem3b  16919  yonedainv  16921  yonffthlem  16922  ablfac1eulem  18471  lsmsp  19086  lsppratlem3  19149  mplcoe1  19465  mdetunilem9  20426  filufint  21724  fmfnfmlem4  21761  hausflim  21785  fclsfnflim  21831  fsumcn  22673  mbfeqalem  23409  itgfsum  23593  jensenlem1  24713  jensenlem2  24714  gsumvsca1  29782  gsumvsca2  29783  ordtconnlem1  29970  vhmcls  31463  mclsppslem  31480  rngunsnply  37743  brtrclfv2  38019