Theorem unssad 4134

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3888   ⊆ wss 3890

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  naddcllem  8605  ersym  8649  findcard2d  9094  finsschain  9262  r0weon  9925  ackbij1lem16  10147  wunex2  10652  sumsplit  15721  fsumabs  15755  fsumiun  15775  mrieqvlemd  17586  yonedalem1  18229  yonedalem21  18230  yonedalem22  18235  yonffthlem  18239  lsmsp  21073  mplcoe1  22025  mdetunilem9  22595  ordtbas  23167  isufil2  23883  ufileu  23894  filufint  23895  fmfnfm  23933  flimclslem  23959  fclsfnflim  24002  flimfnfcls  24003  imasdsf1olem  24348  limcdif  25853  jensenlem1  26964  jensenlem2  26965  jensen  26966  gsumvsca1  33302  gsumvsca2  33303  qsdrngilem  33569  fldgenfldext  33828  evls1fldgencl  33830  fldextrspunlem1  33835  fldextrspunfld  33836  algextdeglem1  33877  algextdeglem2  33878  algextdeglem3  33879  algextdeglem4  33880  constrextdg2lem  33908  constrllcllem  33912  constrlccllem  33913  constrcccllem  33914  ordtconnlem1  34084  ssmcls  35765  mclsppslem  35781  rngunsnply  43615  mptrcllem  44058  clcnvlem  44068  brtrclfv2  44172  isotone1  44493  dvnprodlem1  46392