Theorem prssd 4765

Description: Deduction version of prssi 4764: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypotheses

Ref	Expression
prssd.1	⊢ (𝜑 → 𝐴 ∈ 𝐶)
prssd.2	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
prssd	⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)

Proof of Theorem prssd

Step	Hyp	Ref	Expression
1		prssd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
2		prssd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
3		prssi 4764	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570

This theorem is referenced by:  fpr2g  7166  f1prex  7239  fveqf1o  7257  fr3nr  7726  en2eqpr  9929  en2eleq  9930  r0weon  9934  wuncval2  10670  nehash2  14436  1idssfct  16649  basprssdmsets  17191  mrcun  17588  joinval2  18345  meetval2  18359  0idnsgd  19146  pmtrprfv  19428  pmtrprfv3  19429  symggen  19445  pmtr3ncomlem1  19448  psgnunilem1  19468  lspprcl  20973  lsptpcl  20974  lspprss  20987  lspprid1  20992  lsppratlem2  21146  lsppratlem3  21147  lsppratlem4  21148  drngnidl  21241  drnglpir  21330  mdetralt  22573  topgele  22895  pptbas  22973  isconn2  23379  xpsdsval  24346  itgioo  25783  wilthlem2  27032  perfectlem2  27193  upgrex  29161  upgr1e  29182  uspgr1e  29313  eupth2lems  30308  s2f1  33005  pmtrcnel  33150  pmtrcnel2  33151  fzo0pmtrlast  33153  pmtridf1o  33155  cycpm2tr  33180  cyc3co2  33201  cyc3evpm  33211  cyc3genpmlem  33212  cyc3conja  33218  elrgspnsubrunlem1  33308  gsumind  33405  linds2eq  33441  drngmxidlr  33538  mplmulmvr  33683  esplylem  33710  esplympl  33711  esplyfv1  33713  esplyfval3  33716  esplyfvaln  33718  esplyind  33719  constrllcllem  33896  constrlccllem  33897  poimirlem9  37950  clsk1indlem4  44471  clsk1indlem1  44472  mnuprssd  44696  mnuprdlem4  44702  limsup10exlem  46200  meadjun  46890  clnbgrgrimlem  48409  stgredgiun  48434  stgrnbgr0  48440  grlimprclnbgrvtx  48475  grlimgrtrilem1  48477  gpgiedgdmellem  48522  gpgprismgriedgdmss  48528  line2  49228  line2y  49231  lubprlem  49437  joindm3  49444  meetdm3  49446  toplatjoin  49477  toplatmeet  49478