Theorem prssd 4782

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911  {cpr 4587

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 3446  df-un 3916  df-ss 3928  df-sn 4586  df-pr 4588

This theorem is referenced by:  fpr2g  7167  f1prex  7241  fveqf1o  7259  fr3nr  7728  en2eqpr  9936  en2eleq  9937  r0weon  9941  wuncval2  10676  nehash2  14415  1idssfct  16626  basprssdmsets  17167  mrcun  17563  joinval2  18320  meetval2  18334  0idnsgd  19085  pmtrprfv  19367  pmtrprfv3  19368  symggen  19384  pmtr3ncomlem1  19387  psgnunilem1  19407  lspprcl  20916  lsptpcl  20917  lspprss  20930  lspprid1  20935  lsppratlem2  21090  lsppratlem3  21091  lsppratlem4  21092  drngnidl  21185  drnglpir  21274  mdetralt  22528  topgele  22850  pptbas  22928  isconn2  23334  xpsdsval  24302  itgioo  25750  wilthlem2  27012  perfectlem2  27174  upgrex  29072  upgr1e  29093  uspgr1e  29224  eupth2lems  30217  s2f1  32916  pmtrcnel  33061  pmtrcnel2  33062  fzo0pmtrlast  33064  pmtridf1o  33066  cycpm2tr  33091  cyc3co2  33112  cyc3evpm  33122  cyc3genpmlem  33123  cyc3conja  33129  elrgspnsubrunlem1  33214  linds2eq  33345  drngmxidlr  33442  constrllcllem  33735  constrlccllem  33736  poimirlem9  37616  clsk1indlem4  44026  clsk1indlem1  44027  mnuprssd  44251  mnuprdlem4  44257  limsup10exlem  45763  meadjun  46453  clnbgrgrimlem  47926  stgredgiun  47950  stgrnbgr0  47956  grlimgrtrilem1  47986  gpgiedgdmellem  48030  gpgprismgriedgdmss  48036  line2  48734  line2y  48737  lubprlem  48943  joindm3  48950  meetdm3  48952  toplatjoin  48983  toplatmeet  48984