Theorem prssd 4780

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

Syntax hints:   → wi 4   ∈ wcel 2142   ⊆ wss 3904  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-sn 4583  df-pr 4585

This theorem is referenced by:  fpr2g  7195  f1prex  7268  fveqf1o  7286  fr3nr  7755  en2eqpr  9963  en2eleq  9964  r0weon  9968  wuncval2  10705  nehash2  14487  1idssfct  16714  basprssdmsets  17257  mrcun  17654  joinval2  18411  meetval2  18425  0idnsgd  19212  pmtrprfv  19493  pmtrprfv3  19494  symggen  19510  pmtr3ncomlem1  19513  psgnunilem1  19533  lspprcl  21045  lsptpcl  21046  lspprss  21059  lspprid1  21064  lsppratlem2  21218  lsppratlem3  21219  lsppratlem4  21220  drngnidl  21313  drnglpir  21402  mdetralt  22668  topgele  22990  pptbas  23068  isconn2  23474  xpsdsval  24441  itgioo  25878  wilthlem2  27133  perfectlem2  27294  upgrex  29293  upgr1e  29314  uspgr1e  29445  eupth2lems  30440  s2f1  33123  pmtrcnel  33269  pmtrcnel2  33270  fzo0pmtrlast  33272  pmtridf1o  33274  cycpm2tr  33299  cyc3co2  33320  cyc3evpm  33330  cyc3genpmlem  33331  cyc3conja  33337  elrgspnsubrunlem1  33428  gsumind  33531  linds2eq  33567  drngmxidlr  33666  mplmulmvr  33836  esplylem  33863  esplympl  33864  esplyfv1  33866  esplyfval3  33869  esplyfvaln  33871  esplyind  33872  constrllcllem  34049  constrlccllem  34050  poimirlem9  38128  clsk1indlem4  44620  clsk1indlem1  44621  mnuprssd  44845  mnuprdlem4  44851  limsup10exlem  46346  meadjun  47036  clnbgrgrimlem  48555  stgredgiun  48580  stgrnbgr0  48586  grlimprclnbgrvtx  48621  grlimgrtrilem1  48623  gpgiedgdmellem  48668  gpgprismgriedgdmss  48674  line2  49374  line2y  49377  lubprlem  49583  joindm3  49590  meetdm3  49592  toplatjoin  49623  toplatmeet  49624