Theorem unssad 4194

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3900   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154

This theorem is used by:  naddcllem  8723  ersym  8768  findcard2d  9220  finsschain  9386  r0weon  10130  ackbij1lem16  10351  wunex2  10862  sumsplit  15978  fsumabs  16012  fsumiun  16032  mrieqvlemd  17853  yonedalem1  18496  yonedalem21  18497  yonedalem22  18502  yonffthlem  18506  lsmsp  21412  mplcoe1  22401  mdetunilem9  22990  ordtbas  23565  isufil2  24282  ufileu  24293  filufint  24294  fmfnfm  24332  flimclslem  24358  fclsfnflim  24401  flimfnfcls  24402  imasdsf1olem  24747  limcdif  26251  rngunsnply  26693  jensenlem1  27371  jensenlem2  27372  jensen  27373  gsumvsca1  33886  gsumvsca2  33887  qsdrngilem  34122  evls1rgspncl  34248  fldgenfldext  34411  evls1fldgencl  34413  fldextrspunlem1  34418  fldextrspunfld  34419  algextdeglem1  34460  algextdeglem2  34461  algextdeglem3  34462  algextdeglem4  34463  constrextdg2lem  34491  constrllcllem  34495  constrlccllem  34496  constrcccllem  34497  ordtconnlem1  34667  j0ltalephlem  36048  k1le  36062  ssmcls  36540  mclsppslem  36556  mptrcllem  44874  clcnvlem  44884  brtrclfv2  44988  isotone1  45309  dvnprodlem1  47229  zelaz  49721