Theorem prssd 4827

Description: Deduction version of prssi 4826: 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 4826	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3963  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980  df-sn 4632  df-pr 4634

This theorem is referenced by:  fpr2g  7231  f1prex  7304  fveqf1o  7322  fr3nr  7791  en2eqpr  10045  en2eleq  10046  r0weon  10050  wuncval2  10785  nehash2  14510  1idssfct  16714  basprssdmsets  17258  mrcun  17667  joinval2  18439  meetval2  18453  0idnsgd  19202  pmtrprfv  19486  pmtrprfv3  19487  symggen  19503  pmtr3ncomlem1  19506  psgnunilem1  19526  lspprcl  20994  lsptpcl  20995  lspprss  21008  lspprid1  21013  lsppratlem2  21168  lsppratlem3  21169  lsppratlem4  21170  drngnidl  21271  drnglpir  21360  mdetralt  22630  topgele  22952  pptbas  23031  isconn2  23438  xpsdsval  24407  itgioo  25866  wilthlem2  27127  perfectlem2  27289  upgrex  29124  upgr1e  29145  uspgr1e  29276  eupth2lems  30267  s2f1  32914  pmtrcnel  33092  pmtrcnel2  33093  fzo0pmtrlast  33095  pmtridf1o  33097  cycpm2tr  33122  cyc3co2  33143  cyc3evpm  33153  cyc3genpmlem  33154  cyc3conja  33160  linds2eq  33389  drngmxidlr  33486  poimirlem9  37616  clsk1indlem4  44034  clsk1indlem1  44035  mnuprssd  44265  mnuprdlem4  44271  limsup10exlem  45728  meadjun  46418  clnbgrgrimlem  47839  stgredgiun  47861  stgrnbgr0  47867  grlimgrtrilem1  47897  gpgedgel  47943  line2  48602  line2y  48605  lubprlem  48759  joindm3  48766  meetdm3  48768  toplatjoin  48791  toplatmeet  48792