Theorem unssad 4168

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3924   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943

This theorem is referenced by:  naddcllem  8688  ersym  8731  findcard2d  9180  finsschain  9371  r0weon  10026  ackbij1lem16  10248  wunex2  10752  sumsplit  15784  fsumabs  15817  fsumiun  15837  mrieqvlemd  17641  yonedalem1  18284  yonedalem21  18285  yonedalem22  18290  yonffthlem  18294  lsmsp  21044  mplcoe1  21995  mdetunilem9  22558  ordtbas  23130  isufil2  23846  ufileu  23857  filufint  23858  fmfnfm  23896  flimclslem  23922  fclsfnflim  23965  flimfnfcls  23966  imasdsf1olem  24312  limcdif  25829  jensenlem1  26949  jensenlem2  26950  jensen  26951  gsumvsca1  33223  gsumvsca2  33224  qsdrngilem  33509  fldgenfldext  33709  evls1fldgencl  33711  fldextrspunlem1  33716  fldextrspunfld  33717  algextdeglem1  33751  algextdeglem2  33752  algextdeglem3  33753  algextdeglem4  33754  constrextdg2lem  33782  constrllcllem  33786  constrlccllem  33787  constrcccllem  33788  ordtconnlem1  33955  ssmcls  35589  mclsppslem  35605  rngunsnply  43193  mptrcllem  43637  clcnvlem  43647  brtrclfv2  43751  isotone1  44072  dvnprodlem1  45975