Theorem unssad 4139

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

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

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  naddcllem  8669  ersym  8714  findcard2d  9166  finsschain  9332  r0weon  10072  ackbij1lem16  10293  wunex2  10804  sumsplit  15914  fsumabs  15948  fsumiun  15968  mrieqvlemd  17783  yonedalem1  18426  yonedalem21  18427  yonedalem22  18432  yonffthlem  18436  lsmsp  21341  mplcoe1  22326  mdetunilem9  22915  ordtbas  23490  isufil2  24207  ufileu  24218  filufint  24219  fmfnfm  24257  flimclslem  24283  fclsfnflim  24326  flimfnfcls  24327  imasdsf1olem  24672  limcdif  26176  jensenlem1  27296  jensenlem2  27297  jensen  27298  gsumvsca1  33769  gsumvsca2  33770  qsdrngilem  34000  fldgenfldext  34282  evls1fldgencl  34284  fldextrspunlem1  34289  fldextrspunfld  34290  algextdeglem1  34331  algextdeglem2  34332  algextdeglem3  34333  algextdeglem4  34334  constrextdg2lem  34362  constrllcllem  34366  constrlccllem  34367  constrcccllem  34368  ordtconnlem1  34538  ssmcls  36301  mclsppslem  36317  rngunsnply  44129  mptrcllem  44572  clcnvlem  44582  brtrclfv2  44686  isotone1  45007  dvnprodlem1  46900