Theorem unssbd 4141

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3895   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914

This theorem is referenced by:  eldifpw  7701  naddcllem  8591  ertr  8637  finsschain  9243  r0weon  9903  ackbij1lem16  10125  wunfi  10612  wunex2  10629  hashf1lem2  14363  sumsplit  15675  fsum2dlem  15677  fsumabs  15708  fsumrlim  15718  fsumo1  15719  fsumiun  15728  fprod2dlem  15887  mreexexlem3d  17552  yonedalem1  18178  yonedalem21  18179  yonedalem3a  18180  yonedalem4c  18183  yonedalem22  18184  yonedalem3b  18185  yonedainv  18187  yonffthlem  18188  ablfac1eulem  19986  lsmsp  21020  lsppratlem3  21086  mplcoe1  21972  mdetunilem9  22535  filufint  23835  fmfnfmlem4  23872  hausflim  23896  fclsfnflim  23942  fsumcn  24788  itgfsum  25755  jensenlem1  26924  jensenlem2  26925  gsumvsca1  33195  gsumvsca2  33196  qsdrngilem  33459  evls1fldgencl  33683  fldextrspunlem1  33688  constrextdg2lem  33761  constrllcllem  33765  constrlccllem  33766  constrcccllem  33767  ordtconnlem1  33937  vhmcls  35610  mclsppslem  35627  rngunsnply  43261  brtrclfv2  43819