Theorem prssd 4776

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3899  {cpr 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-sn 4579  df-pr 4581

This theorem is referenced by:  fpr2g  7155  f1prex  7228  fveqf1o  7246  fr3nr  7715  en2eqpr  9915  en2eleq  9916  r0weon  9920  wuncval2  10656  nehash2  14395  1idssfct  16605  basprssdmsets  17146  mrcun  17543  joinval2  18300  meetval2  18314  0idnsgd  19098  pmtrprfv  19380  pmtrprfv3  19381  symggen  19397  pmtr3ncomlem1  19400  psgnunilem1  19420  lspprcl  20927  lsptpcl  20928  lspprss  20941  lspprid1  20946  lsppratlem2  21101  lsppratlem3  21102  lsppratlem4  21103  drngnidl  21196  drnglpir  21285  mdetralt  22550  topgele  22872  pptbas  22950  isconn2  23356  xpsdsval  24323  itgioo  25771  wilthlem2  27033  perfectlem2  27195  upgrex  29114  upgr1e  29135  uspgr1e  29266  eupth2lems  30262  s2f1  32976  pmtrcnel  33120  pmtrcnel2  33121  fzo0pmtrlast  33123  pmtridf1o  33125  cycpm2tr  33150  cyc3co2  33171  cyc3evpm  33181  cyc3genpmlem  33182  cyc3conja  33188  elrgspnsubrunlem1  33278  gsumind  33375  linds2eq  33411  drngmxidlr  33508  mplmulmvr  33653  esplylem  33673  esplympl  33674  esplyfv1  33676  esplyfval3  33679  esplyind  33680  constrllcllem  33858  constrlccllem  33859  poimirlem9  37769  clsk1indlem4  44227  clsk1indlem1  44228  mnuprssd  44452  mnuprdlem4  44458  limsup10exlem  45958  meadjun  46648  clnbgrgrimlem  48121  stgredgiun  48146  stgrnbgr0  48152  grlimprclnbgrvtx  48187  grlimgrtrilem1  48189  gpgiedgdmellem  48234  gpgprismgriedgdmss  48240  line2  48940  line2y  48943  lubprlem  49149  joindm3  49156  meetdm3  49158  toplatjoin  49189  toplatmeet  49190