Theorem prssd 4790

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3906  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-sn 4592  df-pr 4594

This theorem is used by:  fpr2g  7216  f1prex  7291  fveqf1o  7309  fr3nr  7777  en2eqpr  10007  en2eleq  10008  r0weon  10012  wuncval2  10749  nehash2  14531  1idssfct  16762  basprssdmsets  17305  mrcun  17702  joinval2  18459  meetval2  18473  0idnsgd  19283  pmtrprfv  19569  pmtrprfv3  19570  symggen  19586  pmtr3ncomlem1  19589  psgnunilem1  19609  lspprcl  21151  lsptpcl  21152  lspprss  21165  lspprid1  21170  lsppratlem2  21324  lsppratlem3  21325  lsppratlem4  21326  drngnidl  21429  drnglpir  21552  mdetralt  22817  topgele  23139  pptbas  23217  isconn2  23623  xpsdsval  24591  itgioo  26028  wilthlem2  27286  perfectlem2  27447  upgrex  29499  upgr1e  29520  uspgr1e  29654  eupth2lems  30662  s2f1  33335  pmtrcnel  33475  pmtrcnel2  33476  fzo0pmtrlast  33478  pmtridf1o  33480  cycpm2tr  33505  cyc3co2  33526  cyc3evpm  33536  cyc3genpmlem  33537  cyc3conja  33543  elrgspnsubrunlem1  33633  gsumind  33731  linds2eq  33760  drngmxidlr  33826  mplmulmvr  33995  esplylem  34022  esplympl  34023  esplyfv1  34025  esplyfval3  34028  esplyfvaln  34030  esplyind  34031  constrllcllem  34208  constrlccllem  34209  poimirlem9  38339  clsk1indlem4  44830  clsk1indlem1  44831  mnuprssd  45039  mnuprdlem4  45045  limsup10exlem  46546  meadjun  47236  clnbgrgrimlem  48758  stgredgiun  48783  stgrnbgr0  48789  grlimprclnbgrvtx  48824  grlimgrtrilem1  48826  gpgiedgdmellem  48871  gpgprismgriedgdmss  48877  line2  49591  line2y  49594  lubprlem  49799  joindm3  49806  meetdm3  49808  toplatjoin  49839  toplatmeet  49840