Theorem prssd 4780

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  {cpr 4584

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585

This theorem is referenced by:  fpr2g  7167  f1prex  7240  fveqf1o  7258  fr3nr  7727  en2eqpr  9929  en2eleq  9930  r0weon  9934  wuncval2  10670  nehash2  14409  1idssfct  16619  basprssdmsets  17160  mrcun  17557  joinval2  18314  meetval2  18328  0idnsgd  19112  pmtrprfv  19394  pmtrprfv3  19395  symggen  19411  pmtr3ncomlem1  19414  psgnunilem1  19434  lspprcl  20941  lsptpcl  20942  lspprss  20955  lspprid1  20960  lsppratlem2  21115  lsppratlem3  21116  lsppratlem4  21117  drngnidl  21210  drnglpir  21299  mdetralt  22564  topgele  22886  pptbas  22964  isconn2  23370  xpsdsval  24337  itgioo  25785  wilthlem2  27047  perfectlem2  27209  upgrex  29177  upgr1e  29198  uspgr1e  29329  eupth2lems  30325  s2f1  33038  pmtrcnel  33183  pmtrcnel2  33184  fzo0pmtrlast  33186  pmtridf1o  33188  cycpm2tr  33213  cyc3co2  33234  cyc3evpm  33244  cyc3genpmlem  33245  cyc3conja  33251  elrgspnsubrunlem1  33341  gsumind  33438  linds2eq  33474  drngmxidlr  33571  mplmulmvr  33716  esplylem  33743  esplympl  33744  esplyfv1  33746  esplyfval3  33749  esplyfvaln  33751  esplyind  33752  constrllcllem  33930  constrlccllem  33931  poimirlem9  37880  clsk1indlem4  44400  clsk1indlem1  44401  mnuprssd  44625  mnuprdlem4  44631  limsup10exlem  46130  meadjun  46820  clnbgrgrimlem  48293  stgredgiun  48318  stgrnbgr0  48324  grlimprclnbgrvtx  48359  grlimgrtrilem1  48361  gpgiedgdmellem  48406  gpgprismgriedgdmss  48412  line2  49112  line2y  49115  lubprlem  49321  joindm3  49328  meetdm3  49330  toplatjoin  49361  toplatmeet  49362