Theorem prssd 4783

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587

This theorem is used by:  fpr2g  7217  f1prex  7292  fveqf1o  7310  fr3nr  7786  en2eqpr  10086  en2eleq  10087  r0weon  10091  wuncval2  10832  nehash2  14619  1idssfct  16855  basprssdmsets  17399  mrcun  17796  joinval2  18553  meetval2  18567  0idnsgd  19381  pmtrprfv  19667  pmtrprfv3  19668  symggen  19684  pmtr3ncomlem1  19687  psgnunilem1  19707  lspprcl  21253  lsptpcl  21254  lspprss  21267  lspprid1  21272  lsppratlem2  21426  lsppratlem3  21427  lsppratlem4  21428  drngnidl  21531  drnglpir  21656  mdetralt  22923  topgele  23248  pptbas  23326  isconn2  23732  xpsdsval  24700  itgioo  26136  wilthlem2  27396  perfectlem2  27557  upgrex  29670  upgr1e  29691  uspgr1e  29825  eupth2lems  30839  s2f1  33510  pmtrcnel  33650  pmtrcnel2  33651  fzo0pmtrlast  33653  pmtridf1o  33655  cycpm2tr  33680  cyc3co2  33701  cyc3evpm  33711  cyc3genpmlem  33712  cyc3conja  33718  elrgspnsubrunlem1  33808  gsumind  33906  linds2eq  33936  drngmxidlr  34002  mplmulmvr  34171  esplylem  34198  esplympl  34199  esplyfv1  34201  esplyfval3  34204  esplyfvaln  34206  esplyind  34207  constrllcllem  34384  constrlccllem  34385  poimirlem9  38547  clsk1indlem4  45043  clsk1indlem1  45044  mnuprssd  45252  mnuprdlem4  45258  limsup10exlem  46781  meadjun  47471  clnbgrgrimlem  49030  stgredgiun  49055  stgrnbgr0  49061  grlimprclnbgrvtx  49096  grlimgrtrilem1  49098  gpgiedgdmellem  49143  gpgprismgriedgdmss  49149  line2  49863  line2y  49866  lubprlem  50069  joindm3  50076  meetdm3  50078  toplatjoin  50109  toplatmeet  50110