Theorem prssd 4789

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  {cpr 4594

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 3922  df-ss 3934  df-sn 4593  df-pr 4595

This theorem is referenced by:  fpr2g  7188  f1prex  7262  fveqf1o  7280  fr3nr  7751  en2eqpr  9967  en2eleq  9968  r0weon  9972  wuncval2  10707  nehash2  14446  1idssfct  16657  basprssdmsets  17198  mrcun  17590  joinval2  18347  meetval2  18361  0idnsgd  19110  pmtrprfv  19390  pmtrprfv3  19391  symggen  19407  pmtr3ncomlem1  19410  psgnunilem1  19430  lspprcl  20891  lsptpcl  20892  lspprss  20905  lspprid1  20910  lsppratlem2  21065  lsppratlem3  21066  lsppratlem4  21067  drngnidl  21160  drnglpir  21249  mdetralt  22502  topgele  22824  pptbas  22902  isconn2  23308  xpsdsval  24276  itgioo  25724  wilthlem2  26986  perfectlem2  27148  upgrex  29026  upgr1e  29047  uspgr1e  29178  eupth2lems  30174  s2f1  32873  pmtrcnel  33053  pmtrcnel2  33054  fzo0pmtrlast  33056  pmtridf1o  33058  cycpm2tr  33083  cyc3co2  33104  cyc3evpm  33114  cyc3genpmlem  33115  cyc3conja  33121  elrgspnsubrunlem1  33205  linds2eq  33359  drngmxidlr  33456  constrllcllem  33749  constrlccllem  33750  poimirlem9  37630  clsk1indlem4  44040  clsk1indlem1  44041  mnuprssd  44265  mnuprdlem4  44271  limsup10exlem  45777  meadjun  46467  clnbgrgrimlem  47937  stgredgiun  47961  stgrnbgr0  47967  grlimgrtrilem1  47997  gpgiedgdmellem  48041  gpgprismgriedgdmss  48047  line2  48745  line2y  48748  lubprlem  48954  joindm3  48961  meetdm3  48963  toplatjoin  48994  toplatmeet  48995