Theorem prssd 4826

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-sn 4630  df-pr 4632

This theorem is referenced by:  fpr2g  7213  f1prex  7282  fveqf1o  7301  fr3nr  7759  en2eqpr  10002  en2eleq  10003  r0weon  10007  wuncval2  10742  nehash2  14435  1idssfct  16617  basprssdmsets  17157  mrcun  17566  joinval2  18334  meetval2  18348  0idnsgd  19051  pmtrprfv  19321  pmtrprfv3  19322  symggen  19338  pmtr3ncomlem1  19341  psgnunilem1  19361  lspprcl  20589  lsptpcl  20590  lspprss  20603  lspprid1  20608  lsppratlem2  20761  lsppratlem3  20762  lsppratlem4  20763  drngnidl  20854  drnglpir  20891  mdetralt  22110  topgele  22432  pptbas  22511  isconn2  22918  xpsdsval  23887  itgioo  25333  wilthlem2  26573  perfectlem2  26733  upgrex  28352  upgr1e  28373  uspgr1e  28501  eupth2lems  29491  s2f1  32111  pmtrcnel  32250  pmtrcnel2  32251  pmtridf1o  32253  cycpm2tr  32278  cyc3co2  32299  cyc3evpm  32309  cyc3genpmlem  32310  cyc3conja  32316  linds2eq  32497  poimirlem9  36497  clsk1indlem4  42795  clsk1indlem1  42796  mnuprssd  43028  mnuprdlem4  43034  limsup10exlem  44488  meadjun  45178  line2  47438  line2y  47441  lubprlem  47595  joindm3  47602  meetdm3  47604  toplatjoin  47627  toplatmeet  47628