Theorem unssad 4191

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151

This theorem is used by:  naddcllem  8689  ersym  8734  findcard2d  9186  finsschain  9352  r0weon  10095  ackbij1lem16  10316  wunex2  10827  sumsplit  15940  fsumabs  15974  fsumiun  15994  mrieqvlemd  17809  yonedalem1  18452  yonedalem21  18453  yonedalem22  18458  yonffthlem  18462  lsmsp  21367  mplcoe1  22352  mdetunilem9  22941  ordtbas  23516  isufil2  24233  ufileu  24244  filufint  24245  fmfnfm  24283  flimclslem  24309  fclsfnflim  24352  flimfnfcls  24353  imasdsf1olem  24698  limcdif  26202  jensenlem1  27320  jensenlem2  27321  jensen  27322  gsumvsca1  33834  gsumvsca2  33835  qsdrngilem  34065  fldgenfldext  34347  evls1fldgencl  34349  fldextrspunlem1  34354  fldextrspunfld  34355  algextdeglem1  34396  algextdeglem2  34397  algextdeglem3  34398  algextdeglem4  34399  constrextdg2lem  34427  constrllcllem  34431  constrlccllem  34432  constrcccllem  34433  ordtconnlem1  34603  j0ltalephlem  35947  ssmcls  36419  mclsppslem  36435  rngunsnply  44265  mptrcllem  44707  clcnvlem  44717  brtrclfv2  44821  isotone1  45142  dvnprodlem1  47050