Theorem unssad 4147

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
unssad	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem unssad

Step	Hyp	Ref	Expression
1		unssad.1	. . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
2		unss 4144	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
3	1, 2	sylibr 237	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simpld 499	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:  naddcllem  8663  ersym  8708  findcard2d  9152  finsschain  9317  r0weon  9997  ackbij1lem16  10218  wunex2  10724  sumsplit  15821  fsumabs  15855  fsumiun  15875  mrieqvlemd  17686  yonedalem1  18329  yonedalem21  18330  yonedalem22  18335  yonffthlem  18339  lsmsp  21188  mplcoe1  22169  mdetunilem9  22758  ordtbas  23330  isufil2  24046  ufileu  24057  filufint  24058  fmfnfm  24096  flimclslem  24122  fclsfnflim  24165  flimfnfcls  24166  imasdsf1olem  24511  limcdif  26016  jensenlem1  27129  jensenlem2  27130  jensen  27131  gsumvsca1  33524  gsumvsca2  33525  qsdrngilem  33754  fldgenfldext  34036  evls1fldgencl  34038  fldextrspunlem1  34043  fldextrspunfld  34044  algextdeglem1  34085  algextdeglem2  34086  algextdeglem3  34087  algextdeglem4  34088  constrextdg2lem  34116  constrllcllem  34120  constrlccllem  34121  constrcccllem  34122  ordtconnlem1  34292  ssmcls  36037  mclsppslem  36053  rngunsnply  43876  mptrcllem  44319  clcnvlem  44329  brtrclfv2  44433  isotone1  44754  dvnprodlem1  46640