Theorem prssd 4792

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

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-sn 4595  df-pr 4597

This theorem is referenced by:  fpr2g  7210  f1prex  7283  fveqf1o  7301  fr3nr  7771  en2eqpr  9991  en2eleq  9992  r0weon  9996  wuncval2  10732  nehash2  14511  1idssfct  16738  basprssdmsets  17281  mrcun  17678  joinval2  18435  meetval2  18449  0idnsgd  19237  pmtrprfv  19523  pmtrprfv3  19524  symggen  19540  pmtr3ncomlem1  19543  psgnunilem1  19563  lspprcl  21077  lsptpcl  21078  lspprss  21091  lspprid1  21096  lsppratlem2  21250  lsppratlem3  21251  lsppratlem4  21252  drngnidl  21351  drnglpir  21469  mdetralt  22734  topgele  23056  pptbas  23134  isconn2  23540  xpsdsval  24507  itgioo  25944  wilthlem2  27199  perfectlem2  27360  upgrex  29383  upgr1e  29404  uspgr1e  29535  eupth2lems  30530  s2f1  33206  pmtrcnel  33350  pmtrcnel2  33351  fzo0pmtrlast  33353  pmtridf1o  33355  cycpm2tr  33380  cyc3co2  33401  cyc3evpm  33411  cyc3genpmlem  33412  cyc3conja  33418  elrgspnsubrunlem1  33508  gsumind  33608  linds2eq  33638  drngmxidlr  33705  mplmulmvr  33874  esplylem  33901  esplympl  33902  esplyfv1  33904  esplyfval3  33907  esplyfvaln  33909  esplyind  33910  constrllcllem  34087  constrlccllem  34088  poimirlem9  38202  clsk1indlem4  44696  clsk1indlem1  44697  mnuprssd  44905  mnuprdlem4  44911  limsup10exlem  46412  meadjun  47102  clnbgrgrimlem  48621  stgredgiun  48646  stgrnbgr0  48652  grlimprclnbgrvtx  48687  grlimgrtrilem1  48689  gpgiedgdmellem  48734  gpgprismgriedgdmss  48740  line2  49451  line2y  49454  lubprlem  49659  joindm3  49666  meetdm3  49668  toplatjoin  49699  toplatmeet  49700