Theorem unssad 4129

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907

This theorem is referenced by:  naddcllem  8609  ersym  8653  findcard2d  9098  finsschain  9266  r0weon  9932  ackbij1lem16  10154  wunex2  10659  sumsplit  15728  fsumabs  15762  fsumiun  15782  mrieqvlemd  17593  yonedalem1  18236  yonedalem21  18237  yonedalem22  18242  yonffthlem  18246  lsmsp  21083  mplcoe1  22020  mdetunilem9  22610  ordtbas  23182  isufil2  23898  ufileu  23909  filufint  23910  fmfnfm  23948  flimclslem  23974  fclsfnflim  24017  flimfnfcls  24018  imasdsf1olem  24363  limcdif  25868  jensenlem1  26975  jensenlem2  26976  jensen  26977  gsumvsca1  33314  gsumvsca2  33315  qsdrngilem  33584  fldgenfldext  33859  evls1fldgencl  33861  fldextrspunlem1  33866  fldextrspunfld  33867  algextdeglem1  33908  algextdeglem2  33909  algextdeglem3  33910  algextdeglem4  33911  constrextdg2lem  33939  constrllcllem  33943  constrlccllem  33944  constrcccllem  33945  ordtconnlem1  34115  ssmcls  35802  mclsppslem  35818  rngunsnply  43621  mptrcllem  44064  clcnvlem  44074  brtrclfv2  44178  isotone1  44499  dvnprodlem1  46396