Theorem unssad 4148

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

Syntax hints:   → wi 4   ∧ wa 400   ∪ cun 3905   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924

This theorem is referenced by:  naddcllem  8650  ersym  8695  findcard2d  9139  finsschain  9304  r0weon  9984  ackbij1lem16  10205  wunex2  10711  sumsplit  15809  fsumabs  15843  fsumiun  15863  mrieqvlemd  17675  yonedalem1  18318  yonedalem21  18319  yonedalem22  18324  yonffthlem  18328  lsmsp  21176  mplcoe1  22148  mdetunilem9  22738  ordtbas  23310  isufil2  24026  ufileu  24037  filufint  24038  fmfnfm  24076  flimclslem  24102  fclsfnflim  24145  flimfnfcls  24146  imasdsf1olem  24491  limcdif  25996  jensenlem1  27109  jensenlem2  27110  jensen  27111  gsumvsca1  33459  gsumvsca2  33460  qsdrngilem  33693  fldgenfldext  33975  evls1fldgencl  33977  fldextrspunlem1  33982  fldextrspunfld  33983  algextdeglem1  34024  algextdeglem2  34025  algextdeglem3  34026  algextdeglem4  34027  constrextdg2lem  34055  constrllcllem  34059  constrlccllem  34060  constrcccllem  34061  ordtconnlem1  34231  ssmcls  35930  mclsppslem  35946  rngunsnply  43758  mptrcllem  44201  clcnvlem  44211  brtrclfv2  44315  isotone1  44636  dvnprodlem1  46518