Theorem prssd 4787

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3913  {cpr 4593

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918  df-in 3920  df-ss 3930  df-sn 4592  df-pr 4594

This theorem is referenced by:  fpr2g  7166  f1prex  7235  fveqf1o  7254  fr3nr  7711  en2eqpr  9952  en2eleq  9953  r0weon  9957  wuncval2  10692  nehash2  14385  1idssfct  16567  basprssdmsets  17107  mrcun  17516  joinval2  18284  meetval2  18298  0idnsgd  18987  pmtrprfv  19249  pmtrprfv3  19250  symggen  19266  pmtr3ncomlem1  19269  psgnunilem1  19289  lspprcl  20496  lsptpcl  20497  lspprss  20510  lspprid1  20515  lsppratlem2  20668  lsppratlem3  20669  lsppratlem4  20670  drngnidl  20758  drnglpir  20782  mdetralt  21994  topgele  22316  pptbas  22395  isconn2  22802  xpsdsval  23771  itgioo  25217  wilthlem2  26455  perfectlem2  26615  upgrex  28106  upgr1e  28127  uspgr1e  28255  eupth2lems  29245  s2f1  31871  pmtrcnel  32010  pmtrcnel2  32011  pmtridf1o  32013  cycpm2tr  32038  cyc3co2  32059  cyc3evpm  32069  cyc3genpmlem  32070  cyc3conja  32076  linds2eq  32241  poimirlem9  36160  clsk1indlem4  42438  clsk1indlem1  42439  mnuprssd  42671  mnuprdlem4  42677  limsup10exlem  44133  meadjun  44823  line2  46958  line2y  46961  lubprlem  47115  joindm3  47122  meetdm3  47124  toplatjoin  47147  toplatmeet  47148