Theorem prssd 4847

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3976  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651

This theorem is referenced by:  fpr2g  7248  f1prex  7320  fveqf1o  7338  fr3nr  7807  en2eqpr  10076  en2eleq  10077  r0weon  10081  wuncval2  10816  nehash2  14523  1idssfct  16727  basprssdmsets  17271  mrcun  17680  joinval2  18451  meetval2  18465  0idnsgd  19211  pmtrprfv  19495  pmtrprfv3  19496  symggen  19512  pmtr3ncomlem1  19515  psgnunilem1  19535  lspprcl  20999  lsptpcl  21000  lspprss  21013  lspprid1  21018  lsppratlem2  21173  lsppratlem3  21174  lsppratlem4  21175  drngnidl  21276  drnglpir  21365  mdetralt  22635  topgele  22957  pptbas  23036  isconn2  23443  xpsdsval  24412  itgioo  25871  wilthlem2  27130  perfectlem2  27292  upgrex  29127  upgr1e  29148  uspgr1e  29279  eupth2lems  30270  s2f1  32911  pmtrcnel  33082  pmtrcnel2  33083  fzo0pmtrlast  33085  pmtridf1o  33087  cycpm2tr  33112  cyc3co2  33133  cyc3evpm  33143  cyc3genpmlem  33144  cyc3conja  33150  linds2eq  33374  drngmxidlr  33471  poimirlem9  37589  clsk1indlem4  44006  clsk1indlem1  44007  mnuprssd  44238  mnuprdlem4  44244  limsup10exlem  45693  meadjun  46383  clnbgrgrimlem  47785  grlimgrtrilem1  47818  line2  48486  line2y  48489  lubprlem  48642  joindm3  48649  meetdm3  48651  toplatjoin  48674  toplatmeet  48675