Theorem prssd 4771

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3897  {cpr 4575

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914  df-sn 4574  df-pr 4576

This theorem is referenced by:  fpr2g  7145  f1prex  7218  fveqf1o  7236  fr3nr  7705  en2eqpr  9898  en2eleq  9899  r0weon  9903  wuncval2  10638  nehash2  14381  1idssfct  16591  basprssdmsets  17132  mrcun  17528  joinval2  18285  meetval2  18299  0idnsgd  19083  pmtrprfv  19365  pmtrprfv3  19366  symggen  19382  pmtr3ncomlem1  19385  psgnunilem1  19405  lspprcl  20911  lsptpcl  20912  lspprss  20925  lspprid1  20930  lsppratlem2  21085  lsppratlem3  21086  lsppratlem4  21087  drngnidl  21180  drnglpir  21269  mdetralt  22523  topgele  22845  pptbas  22923  isconn2  23329  xpsdsval  24296  itgioo  25744  wilthlem2  27006  perfectlem2  27168  upgrex  29070  upgr1e  29091  uspgr1e  29222  eupth2lems  30218  s2f1  32926  pmtrcnel  33058  pmtrcnel2  33059  fzo0pmtrlast  33061  pmtridf1o  33063  cycpm2tr  33088  cyc3co2  33109  cyc3evpm  33119  cyc3genpmlem  33120  cyc3conja  33126  elrgspnsubrunlem1  33214  gsumind  33310  linds2eq  33346  drngmxidlr  33443  esplylem  33587  esplympl  33588  esplyfv1  33590  constrllcllem  33765  constrlccllem  33766  poimirlem9  37679  clsk1indlem4  44147  clsk1indlem1  44148  mnuprssd  44372  mnuprdlem4  44378  limsup10exlem  45880  meadjun  46570  clnbgrgrimlem  48043  stgredgiun  48068  stgrnbgr0  48074  grlimprclnbgrvtx  48109  grlimgrtrilem1  48111  gpgiedgdmellem  48156  gpgprismgriedgdmss  48162  line2  48863  line2y  48866  lubprlem  49072  joindm3  49079  meetdm3  49081  toplatjoin  49112  toplatmeet  49113