Theorem unssad 3934

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

Syntax hints:   → wi 4   ∧ wa 383   ∪ cun 3714   ⊆ wss 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-un 3721  df-in 3723  df-ss 3730

This theorem is referenced by:  ersym  7926  findcard2d  8370  finsschain  8441  r0weon  9046  ackbij1lem16  9270  wunex2  9773  sumsplit  14719  fsumabs  14753  fsumiun  14773  mrieqvlemd  16512  yonedalem1  17134  yonedalem21  17135  yonedalem22  17140  yonffthlem  17144  lsmsp  19309  mplcoe1  19688  mdetunilem9  20649  ordtbas  21219  isufil2  21934  ufileu  21945  filufint  21946  fmfnfm  21984  flimclslem  22010  fclsfnflim  22053  flimfnfcls  22054  imasdsf1olem  22400  mbfeqalem  23629  limcdif  23860  jensenlem1  24934  jensenlem2  24935  jensen  24936  gsumvsca1  30113  gsumvsca2  30114  ordtconnlem1  30301  ssmcls  31793  mclsppslem  31809  rngunsnply  38264  mptrcllem  38441  clcnvlem  38451  brtrclfv2  38540  isotone1  38867  dvnprodlem1  40683