Theorem unssad 4142

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919

This theorem is used by:  naddcllem  8668  ersym  8713  findcard2d  9165  finsschain  9330  r0weon  10019  ackbij1lem16  10240  wunex2  10751  sumsplit  15858  fsumabs  15892  fsumiun  15912  mrieqvlemd  17723  yonedalem1  18366  yonedalem21  18367  yonedalem22  18372  yonffthlem  18376  lsmsp  21276  mplcoe1  22259  mdetunilem9  22848  ordtbas  23423  isufil2  24140  ufileu  24151  filufint  24152  fmfnfm  24190  flimclslem  24216  fclsfnflim  24259  flimfnfcls  24260  imasdsf1olem  24605  limcdif  26110  jensenlem1  27231  jensenlem2  27232  jensen  27233  gsumvsca1  33674  gsumvsca2  33675  qsdrngilem  33904  fldgenfldext  34186  evls1fldgencl  34188  fldextrspunlem1  34193  fldextrspunfld  34194  algextdeglem1  34235  algextdeglem2  34236  algextdeglem3  34237  algextdeglem4  34238  constrextdg2lem  34266  constrllcllem  34270  constrlccllem  34271  constrcccllem  34272  ordtconnlem1  34442  ssmcls  36154  mclsppslem  36170  rngunsnply  44018  mptrcllem  44461  clcnvlem  44471  brtrclfv2  44575  isotone1  44896  dvnprodlem1  46782