Theorem unssad 4133

Description: If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4130. Partial converse of unssd 4132. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
unssad.1	⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)

Assertion

Ref	Expression
unssad	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem unssad

Step	Hyp	Ref	Expression
1		unssad.1	. . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
2		unss 4130	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
3	1, 2	sylibr 234	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simpld 494	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3887   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906

This theorem is referenced by:  naddcllem  8612  ersym  8656  findcard2d  9101  finsschain  9269  r0weon  9934  ackbij1lem16  10156  wunex2  10661  sumsplit  15730  fsumabs  15764  fsumiun  15784  mrieqvlemd  17595  yonedalem1  18238  yonedalem21  18239  yonedalem22  18244  yonffthlem  18248  lsmsp  21081  mplcoe1  22015  mdetunilem9  22585  ordtbas  23157  isufil2  23873  ufileu  23884  filufint  23885  fmfnfm  23923  flimclslem  23949  fclsfnflim  23992  flimfnfcls  23993  imasdsf1olem  24338  limcdif  25843  jensenlem1  26950  jensenlem2  26951  jensen  26952  gsumvsca1  33287  gsumvsca2  33288  qsdrngilem  33554  fldgenfldext  33812  evls1fldgencl  33814  fldextrspunlem1  33819  fldextrspunfld  33820  algextdeglem1  33861  algextdeglem2  33862  algextdeglem3  33863  algextdeglem4  33864  constrextdg2lem  33892  constrllcllem  33896  constrlccllem  33897  constrcccllem  33898  ordtconnlem1  34068  ssmcls  35749  mclsppslem  35765  rngunsnply  43597  mptrcllem  44040  clcnvlem  44050  brtrclfv2  44154  isotone1  44475  dvnprodlem1  46374