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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916

This theorem is used by:  eldifpw  7767  naddcllem  8664  ertr  8712  finsschain  9326  r0weon  10015  ackbij1lem16  10236  wunfi  10730  wunex2  10747  hashf1lem2  14521  sumsplit  15854  fsum2dlem  15856  fsumabs  15888  fsumrlim  15898  fsumo1  15899  fsumiun  15908  fprod2dlem  16067  mreexexlem3d  17734  yonedalem1  18360  yonedalem21  18361  yonedalem3a  18362  yonedalem4c  18365  yonedalem22  18366  yonedalem3b  18367  yonedainv  18369  yonffthlem  18370  ablfac1eulem  20201  lsmsp  21270  lsppratlem3  21336  mplcoe1  22253  mdetunilem9  22842  filufint  24146  fmfnfmlem4  24183  hausflim  24207  fclsfnflim  24253  fsumcn  25098  itgfsum  26054  jensenlem1  27223  jensenlem2  27224  gsumvsca1  33666  gsumvsca2  33667  qsdrngilem  33896  evls1fldgencl  34180  fldextrspunlem1  34185  constrextdg2lem  34258  constrllcllem  34262  constrlccllem  34263  constrcccllem  34264  ordtconnlem1  34434  vhmcls  36145  mclsppslem  36162  rngunsnply  44010  brtrclfv2  44567