Theorem unssad 3752

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

Syntax hints:   → wi 4   ∧ wa 383   ∪ cun 3538   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554

This theorem is referenced by:  ersym  7641  findcard2d  8087  finsschain  8156  r0weon  8718  ackbij1lem16  8940  wunex2  9439  sumsplit  14341  fsumabs  14374  fsumiun  14394  mrieqvlemd  16112  yonedalem1  16735  yonedalem21  16736  yonedalem22  16741  yonffthlem  16745  lsmsp  18907  mplcoe1  19286  mdetunilem9  20245  ordtbas  20806  isufil2  21522  ufileu  21533  filufint  21534  fmfnfm  21572  flimclslem  21598  fclsfnflim  21641  flimfnfcls  21642  imasdsf1olem  21988  mbfeqalem  23215  limcdif  23446  jensenlem1  24513  jensenlem2  24514  jensen  24515  gsumvsca1  29113  gsumvsca2  29114  ordtconlem1  29298  ssmcls  30718  mclsppslem  30734  rngunsnply  36762  mptrcllem  36939  clcnvlem  36949  brtrclfv2  37038  isotone1  37366  dvnprodlem1  38836