Theorem prssd 4761

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

Syntax hints:   → wi 4   ∈ wcel 2104   ⊆ wss 3892  {cpr 4567

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-un 3897  df-in 3899  df-ss 3909  df-sn 4566  df-pr 4568

This theorem is referenced by:  fpr2g  7119  f1prex  7188  fveqf1o  7207  fr3nr  7654  en2eqpr  9809  en2eleq  9810  r0weon  9814  wuncval2  10549  nehash2  14233  1idssfct  16430  basprssdmsets  16970  mrcun  17376  joinval2  18144  meetval2  18158  0idnsgd  18844  pmtrprfv  19106  pmtrprfv3  19107  symggen  19123  pmtr3ncomlem1  19126  psgnunilem1  19146  lspprcl  20285  lsptpcl  20286  lspprss  20299  lspprid1  20304  lsppratlem2  20455  lsppratlem3  20456  lsppratlem4  20457  drngnidl  20545  drnglpir  20569  mdetralt  21802  topgele  22124  pptbas  22203  isconn2  22610  xpsdsval  23579  itgioo  25025  wilthlem2  26263  perfectlem2  26423  upgrex  27507  upgr1e  27528  uspgr1e  27656  eupth2lems  28647  s2f1  31264  pmtrcnel  31403  pmtrcnel2  31404  pmtridf1o  31406  cycpm2tr  31431  cyc3co2  31452  cyc3evpm  31462  cyc3genpmlem  31463  cyc3conja  31469  linds2eq  31620  poimirlem9  35830  clsk1indlem4  41692  clsk1indlem1  41693  mnuprssd  41925  mnuprdlem4  41931  limsup10exlem  43362  meadjun  44050  line2  46156  line2y  46159  lubprlem  46314  joindm3  46321  meetdm3  46323  toplatjoin  46346  toplatmeet  46347