Theorem unssad 4149

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∪ cun 3906   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925

This theorem is used by:  naddcllem  8671  ersym  8716  findcard2d  9161  finsschain  9326  r0weon  10015  ackbij1lem16  10236  wunex2  10741  sumsplit  15845  fsumabs  15879  fsumiun  15899  mrieqvlemd  17710  yonedalem1  18353  yonedalem21  18354  yonedalem22  18359  yonffthlem  18363  lsmsp  21244  mplcoe1  22225  mdetunilem9  22814  ordtbas  23386  isufil2  24102  ufileu  24113  filufint  24114  fmfnfm  24152  flimclslem  24178  fclsfnflim  24221  flimfnfcls  24222  imasdsf1olem  24567  limcdif  26072  jensenlem1  27188  jensenlem2  27189  jensen  27190  gsumvsca1  33577  gsumvsca2  33578  qsdrngilem  33807  fldgenfldext  34089  evls1fldgencl  34091  fldextrspunlem1  34096  fldextrspunfld  34097  algextdeglem1  34138  algextdeglem2  34139  algextdeglem3  34140  algextdeglem4  34141  constrextdg2lem  34169  constrllcllem  34173  constrlccllem  34174  constrcccllem  34175  ordtconnlem1  34345  ssmcls  36080  mclsppslem  36096  rngunsnply  43937  mptrcllem  44380  clcnvlem  44390  brtrclfv2  44494  isotone1  44815  dvnprodlem1  46701