Theorem unssbd 4046

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

Syntax hints:   → wi 4   ∧ wa 387   ∪ cun 3820   ⊆ wss 3822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-v 3410  df-un 3827  df-in 3829  df-ss 3836

This theorem is referenced by:  eldifpw  7305  ertr  8102  finsschain  8624  r0weon  9230  ackbij1lem16  9453  wunfi  9939  wunex2  9956  hashf1lem2  13625  sumsplit  14981  fsum2dlem  14983  fsumabs  15014  fsumrlim  15024  fsumo1  15025  fsumiun  15034  fprod2dlem  15192  mreexexlem3d  16787  yonedalem1  17392  yonedalem21  17393  yonedalem3a  17394  yonedalem4c  17397  yonedalem22  17398  yonedalem3b  17399  yonedainv  17401  yonffthlem  17402  ablfac1eulem  18956  lsmsp  19592  lsppratlem3  19655  mplcoe1  19971  mdetunilem9  20948  filufint  22247  fmfnfmlem4  22284  hausflim  22308  fclsfnflim  22354  fsumcn  23196  itgfsum  24145  jensenlem1  25281  jensenlem2  25282  gsumvsca1  30557  gsumvsca2  30558  ordtconnlem1  30843  vhmcls  32370  mclsppslem  32387  rngunsnply  39207  brtrclfv2  39473