Theorem unssbd 4140

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  eldifpw  7780  naddcllem  8678  ertr  8726  finsschain  9341  r0weon  10084  ackbij1lem16  10305  wunfi  10799  wunex2  10816  hashf1lem2  14594  sumsplit  15927  fsum2dlem  15929  fsumabs  15961  fsumrlim  15971  fsumo1  15972  fsumiun  15981  fprod2dlem  16140  mreexexlem3d  17813  yonedalem1  18439  yonedalem21  18440  yonedalem3a  18441  yonedalem4c  18444  yonedalem22  18445  yonedalem3b  18446  yonedainv  18448  yonffthlem  18449  ablfac1eulem  20281  lsmsp  21354  lsppratlem3  21420  mplcoe1  22339  mdetunilem9  22928  filufint  24232  fmfnfmlem4  24269  hausflim  24293  fclsfnflim  24339  fsumcn  25184  itgfsum  26140  jensenlem1  27307  jensenlem2  27308  gsumvsca1  33780  gsumvsca2  33781  qsdrngilem  34011  evls1fldgencl  34295  fldextrspunlem1  34300  constrextdg2lem  34373  constrllcllem  34377  constrlccllem  34378  constrcccllem  34379  ordtconnlem1  34549  vhmcls  36310  mclsppslem  36327  rngunsnply  44155  brtrclfv2  44712