Theorem unssbd 4143

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919

This theorem is used by:  eldifpw  7770  naddcllem  8667  ertr  8715  finsschain  9329  r0weon  10018  ackbij1lem16  10239  wunfi  10733  wunex2  10750  hashf1lem2  14523  sumsplit  15856  fsum2dlem  15858  fsumabs  15890  fsumrlim  15900  fsumo1  15901  fsumiun  15910  fprod2dlem  16071  mreexexlem3d  17738  yonedalem1  18364  yonedalem21  18365  yonedalem3a  18366  yonedalem4c  18369  yonedalem22  18370  yonedalem3b  18371  yonedainv  18373  yonffthlem  18374  ablfac1eulem  20202  lsmsp  21271  lsppratlem3  21337  mplcoe1  22254  mdetunilem9  22843  filufint  24147  fmfnfmlem4  24184  hausflim  24208  fclsfnflim  24254  fsumcn  25099  itgfsum  26056  jensenlem1  27221  jensenlem2  27222  gsumvsca1  33653  gsumvsca2  33654  qsdrngilem  33883  evls1fldgencl  34167  fldextrspunlem1  34172  constrextdg2lem  34245  constrllcllem  34249  constrlccllem  34250  constrcccllem  34251  ordtconnlem1  34421  vhmcls  36132  mclsppslem  36149  rngunsnply  43997  brtrclfv2  44554