Theorem prssd 4781

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3900  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  fpr2g  7227  f1prex  7302  fveqf1o  7320  fr3nr  7796  en2eqpr  10099  en2eleq  10100  r0weon  10104  wuncval2  10845  nehash2  14632  1idssfct  16870  basprssdmsets  17414  mrcun  17811  joinval2  18568  meetval2  18582  0idnsgd  19396  pmtrprfv  19682  pmtrprfv3  19683  symggen  19699  pmtr3ncomlem1  19702  psgnunilem1  19722  lspprcl  21268  lsptpcl  21269  lspprss  21282  lspprid1  21287  lsppratlem2  21441  lsppratlem3  21442  lsppratlem4  21443  drngnidl  21546  drnglpir  21671  mdetralt  22938  topgele  23263  pptbas  23341  isconn2  23747  xpsdsval  24715  itgioo  26151  wilthlem2  27411  perfectlem2  27572  upgrex  29685  upgr1e  29706  uspgr1e  29840  eupth2lems  30854  s2f1  33566  pmtrcnel  33706  pmtrcnel2  33707  fzo0pmtrlast  33709  pmtridf1o  33711  cycpm2tr  33736  cyc3co2  33757  cyc3evpm  33767  cyc3genpmlem  33768  cyc3conja  33774  elrgspnsubrunlem1  33864  gsumind  33962  linds2eq  33992  drngmxidlr  34058  mplmulmvr  34227  esplylem  34254  esplympl  34255  esplyfv1  34257  esplyfval3  34260  esplyfvaln  34262  esplyind  34263  constrllcllem  34440  constrlccllem  34441  poimirlem9  38690  clsk1indlem4  45187  clsk1indlem1  45188  mnuprssd  45396  mnuprdlem4  45402  limsup10exlem  46924  meadjun  47614  clnbgrgrimlem  49173  stgredgiun  49198  stgrnbgr0  49204  grlimprclnbgrvtx  49239  grlimgrtrilem1  49241  gpgiedgdmellem  49286  gpgprismgriedgdmss  49292  line2  50006  lubprlem  50218  joindm3  50225  meetdm3  50227  toplatjoin  50258  toplatmeet  50259