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 584	1 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3916  {cpr 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3921  df-ss 3933  df-sn 4592  df-pr 4594

This theorem is referenced by:  fpr2g  7187  f1prex  7261  fveqf1o  7279  fr3nr  7750  en2eqpr  9966  en2eleq  9967  r0weon  9971  wuncval2  10706  nehash2  14445  1idssfct  16656  basprssdmsets  17197  mrcun  17589  joinval2  18346  meetval2  18360  0idnsgd  19109  pmtrprfv  19389  pmtrprfv3  19390  symggen  19406  pmtr3ncomlem1  19409  psgnunilem1  19429  lspprcl  20890  lsptpcl  20891  lspprss  20904  lspprid1  20909  lsppratlem2  21064  lsppratlem3  21065  lsppratlem4  21066  drngnidl  21159  drnglpir  21248  mdetralt  22501  topgele  22823  pptbas  22901  isconn2  23307  xpsdsval  24275  itgioo  25723  wilthlem2  26985  perfectlem2  27147  upgrex  29025  upgr1e  29046  uspgr1e  29177  eupth2lems  30173  s2f1  32872  pmtrcnel  33052  pmtrcnel2  33053  fzo0pmtrlast  33055  pmtridf1o  33057  cycpm2tr  33082  cyc3co2  33103  cyc3evpm  33113  cyc3genpmlem  33114  cyc3conja  33120  elrgspnsubrunlem1  33204  linds2eq  33358  drngmxidlr  33455  constrllcllem  33748  constrlccllem  33749  poimirlem9  37618  clsk1indlem4  44026  clsk1indlem1  44027  mnuprssd  44251  mnuprdlem4  44257  limsup10exlem  45763  meadjun  46453  clnbgrgrimlem  47923  stgredgiun  47947  stgrnbgr0  47953  grlimgrtrilem1  47983  gpgiedgdmellem  48027  gpgprismgriedgdmss  48033  line2  48731  line2y  48734  lubprlem  48940  joindm3  48947  meetdm3  48949  toplatjoin  48980  toplatmeet  48981