Theorem prssd 4786

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  {cpr 4591

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-sn 4590  df-pr 4592

This theorem is referenced by:  fpr2g  7185  f1prex  7259  fveqf1o  7277  fr3nr  7748  en2eqpr  9960  en2eleq  9961  r0weon  9965  wuncval2  10700  nehash2  14439  1idssfct  16650  basprssdmsets  17191  mrcun  17583  joinval2  18340  meetval2  18354  0idnsgd  19103  pmtrprfv  19383  pmtrprfv3  19384  symggen  19400  pmtr3ncomlem1  19403  psgnunilem1  19423  lspprcl  20884  lsptpcl  20885  lspprss  20898  lspprid1  20903  lsppratlem2  21058  lsppratlem3  21059  lsppratlem4  21060  drngnidl  21153  drnglpir  21242  mdetralt  22495  topgele  22817  pptbas  22895  isconn2  23301  xpsdsval  24269  itgioo  25717  wilthlem2  26979  perfectlem2  27141  upgrex  29019  upgr1e  29040  uspgr1e  29171  eupth2lems  30167  s2f1  32866  pmtrcnel  33046  pmtrcnel2  33047  fzo0pmtrlast  33049  pmtridf1o  33051  cycpm2tr  33076  cyc3co2  33097  cyc3evpm  33107  cyc3genpmlem  33108  cyc3conja  33114  elrgspnsubrunlem1  33198  linds2eq  33352  drngmxidlr  33449  constrllcllem  33742  constrlccllem  33743  poimirlem9  37623  clsk1indlem4  44033  clsk1indlem1  44034  mnuprssd  44258  mnuprdlem4  44264  limsup10exlem  45770  meadjun  46460  clnbgrgrimlem  47933  stgredgiun  47957  stgrnbgr0  47963  grlimgrtrilem1  47993  gpgiedgdmellem  48037  gpgprismgriedgdmss  48043  line2  48741  line2y  48744  lubprlem  48950  joindm3  48957  meetdm3  48959  toplatjoin  48990  toplatmeet  48991