Theorem unssbd 4148

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

Syntax hints:   → wi 4   ∧ wa 400   ∪ cun 3904   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923

This theorem is referenced by:  eldifpw  7768  naddcllem  8663  ertr  8711  finsschain  9317  r0weon  9997  ackbij1lem16  10218  wunfi  10707  wunex2  10724  hashf1lem2  14495  sumsplit  15821  fsum2dlem  15823  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  fprod2dlem  16036  mreexexlem3d  17703  yonedalem1  18329  yonedalem21  18330  yonedalem3a  18331  yonedalem4c  18334  yonedalem22  18335  yonedalem3b  18336  yonedainv  18338  yonffthlem  18339  ablfac1eulem  20145  lsmsp  21188  lsppratlem3  21254  mplcoe1  22169  mdetunilem9  22758  filufint  24058  fmfnfmlem4  24095  hausflim  24119  fclsfnflim  24165  fsumcn  25010  itgfsum  25967  jensenlem1  27132  jensenlem2  27133  gsumvsca1  33527  gsumvsca2  33528  qsdrngilem  33757  evls1fldgencl  34041  fldextrspunlem1  34046  constrextdg2lem  34119  constrllcllem  34123  constrlccllem  34124  constrcccllem  34125  ordtconnlem1  34295  vhmcls  36039  mclsppslem  36056  rngunsnply  43879  brtrclfv2  44436