Theorem prssd 4766

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  {cpr 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571

This theorem is referenced by:  fpr2g  7160  f1prex  7233  fveqf1o  7251  fr3nr  7720  en2eqpr  9923  en2eleq  9924  r0weon  9928  wuncval2  10664  nehash2  14430  1idssfct  16643  basprssdmsets  17185  mrcun  17582  joinval2  18339  meetval2  18353  0idnsgd  19140  pmtrprfv  19422  pmtrprfv3  19423  symggen  19439  pmtr3ncomlem1  19442  psgnunilem1  19462  lspprcl  20967  lsptpcl  20968  lspprss  20981  lspprid1  20986  lsppratlem2  21141  lsppratlem3  21142  lsppratlem4  21143  drngnidl  21236  drnglpir  21325  mdetralt  22586  topgele  22908  pptbas  22986  isconn2  23392  xpsdsval  24359  itgioo  25796  wilthlem2  27049  perfectlem2  27210  upgrex  29178  upgr1e  29199  uspgr1e  29330  eupth2lems  30326  s2f1  33023  pmtrcnel  33168  pmtrcnel2  33169  fzo0pmtrlast  33171  pmtridf1o  33173  cycpm2tr  33198  cyc3co2  33219  cyc3evpm  33229  cyc3genpmlem  33230  cyc3conja  33236  elrgspnsubrunlem1  33326  gsumind  33423  linds2eq  33459  drngmxidlr  33556  mplmulmvr  33701  esplylem  33728  esplympl  33729  esplyfv1  33731  esplyfval3  33734  esplyfvaln  33736  esplyind  33737  constrllcllem  33915  constrlccllem  33916  poimirlem9  37967  clsk1indlem4  44492  clsk1indlem1  44493  mnuprssd  44717  mnuprdlem4  44723  limsup10exlem  46221  meadjun  46911  clnbgrgrimlem  48424  stgredgiun  48449  stgrnbgr0  48455  grlimprclnbgrvtx  48490  grlimgrtrilem1  48492  gpgiedgdmellem  48537  gpgprismgriedgdmss  48543  line2  49243  line2y  49246  lubprlem  49452  joindm3  49459  meetdm3  49461  toplatjoin  49492  toplatmeet  49493