Theorem prssd 4788

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3905  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-sn 4590  df-pr 4592

This theorem is referenced by:  fpr2g  7209  f1prex  7282  fveqf1o  7300  fr3nr  7767  en2eqpr  9987  en2eleq  9988  r0weon  9992  wuncval2  10727  nehash2  14507  1idssfct  16733  basprssdmsets  17276  mrcun  17673  joinval2  18430  meetval2  18444  0idnsgd  19232  pmtrprfv  19518  pmtrprfv3  19519  symggen  19535  pmtr3ncomlem1  19538  psgnunilem1  19558  lspprcl  21099  lsptpcl  21100  lspprss  21113  lspprid1  21118  lsppratlem2  21272  lsppratlem3  21273  lsppratlem4  21274  drngnidl  21377  drnglpir  21500  mdetralt  22765  topgele  23087  pptbas  23165  isconn2  23571  xpsdsval  24538  itgioo  25975  wilthlem2  27233  perfectlem2  27394  upgrex  29442  upgr1e  29463  uspgr1e  29594  eupth2lems  30589  s2f1  33265  pmtrcnel  33409  pmtrcnel2  33410  fzo0pmtrlast  33412  pmtridf1o  33414  cycpm2tr  33439  cyc3co2  33460  cyc3evpm  33470  cyc3genpmlem  33471  cyc3conja  33477  elrgspnsubrunlem1  33567  gsumind  33665  linds2eq  33694  drngmxidlr  33760  mplmulmvr  33929  esplylem  33956  esplympl  33957  esplyfv1  33959  esplyfval3  33962  esplyfvaln  33964  esplyind  33965  constrllcllem  34142  constrlccllem  34143  poimirlem9  38300  clsk1indlem4  44790  clsk1indlem1  44791  mnuprssd  44999  mnuprdlem4  45005  limsup10exlem  46506  meadjun  47196  clnbgrgrimlem  48718  stgredgiun  48743  stgrnbgr0  48749  grlimprclnbgrvtx  48784  grlimgrtrilem1  48786  gpgiedgdmellem  48831  gpgprismgriedgdmss  48837  line2  49552  line2y  49555  lubprlem  49760  joindm3  49767  meetdm3  49769  toplatjoin  49800  toplatmeet  49801