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 234	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simpld 494	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3896   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915

This theorem is referenced by:  naddcllem  8597  ersym  8640  findcard2d  9083  finsschain  9250  r0weon  9910  ackbij1lem16  10132  wunex2  10636  sumsplit  15677  fsumabs  15710  fsumiun  15730  mrieqvlemd  17537  yonedalem1  18180  yonedalem21  18181  yonedalem22  18186  yonffthlem  18190  lsmsp  21022  mplcoe1  21973  mdetunilem9  22536  ordtbas  23108  isufil2  23824  ufileu  23835  filufint  23836  fmfnfm  23874  flimclslem  23900  fclsfnflim  23943  flimfnfcls  23944  imasdsf1olem  24289  limcdif  25805  jensenlem1  26925  jensenlem2  26926  jensen  26927  gsumvsca1  33202  gsumvsca2  33203  qsdrngilem  33466  fldgenfldext  33702  evls1fldgencl  33704  fldextrspunlem1  33709  fldextrspunfld  33710  algextdeglem1  33751  algextdeglem2  33752  algextdeglem3  33753  algextdeglem4  33754  constrextdg2lem  33782  constrllcllem  33786  constrlccllem  33787  constrcccllem  33788  ordtconnlem1  33958  ssmcls  35632  mclsppslem  35648  rngunsnply  43286  mptrcllem  43730  clcnvlem  43740  brtrclfv2  43844  isotone1  44165  dvnprodlem1  46068