Theorem prssd 4803

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3931  {cpr 4608

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948  df-sn 4607  df-pr 4609

This theorem is referenced by:  fpr2g  7208  f1prex  7282  fveqf1o  7300  fr3nr  7771  en2eqpr  10026  en2eleq  10027  r0weon  10031  wuncval2  10766  nehash2  14497  1idssfct  16704  basprssdmsets  17245  mrcun  17639  joinval2  18396  meetval2  18410  0idnsgd  19159  pmtrprfv  19439  pmtrprfv3  19440  symggen  19456  pmtr3ncomlem1  19459  psgnunilem1  19479  lspprcl  20940  lsptpcl  20941  lspprss  20954  lspprid1  20959  lsppratlem2  21114  lsppratlem3  21115  lsppratlem4  21116  drngnidl  21209  drnglpir  21298  mdetralt  22551  topgele  22873  pptbas  22951  isconn2  23357  xpsdsval  24325  itgioo  25774  wilthlem2  27036  perfectlem2  27198  upgrex  29076  upgr1e  29097  uspgr1e  29228  eupth2lems  30224  s2f1  32925  pmtrcnel  33105  pmtrcnel2  33106  fzo0pmtrlast  33108  pmtridf1o  33110  cycpm2tr  33135  cyc3co2  33156  cyc3evpm  33166  cyc3genpmlem  33167  cyc3conja  33173  elrgspnsubrunlem1  33247  linds2eq  33401  drngmxidlr  33498  constrllcllem  33791  constrlccllem  33792  poimirlem9  37658  clsk1indlem4  44035  clsk1indlem1  44036  mnuprssd  44260  mnuprdlem4  44266  limsup10exlem  45768  meadjun  46458  clnbgrgrimlem  47913  stgredgiun  47937  stgrnbgr0  47943  grlimgrtrilem1  47973  gpgiedgdmellem  48017  gpgprismgriedgdmss  48023  line2  48699  line2y  48702  lubprlem  48903  joindm3  48910  meetdm3  48912  toplatjoin  48943  toplatmeet  48944