Theorem prssd 4753

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883  {cpr 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-sn 4556  df-pr 4558

This theorem is referenced by:  fpr2g  7155  f1prex  7228  fveqf1o  7246  fr3nr  7715  en2eqpr  9920  en2eleq  9921  r0weon  9925  wuncval2  10661  nehash2  14427  1idssfct  16640  basprssdmsets  17182  mrcun  17579  joinval2  18336  meetval2  18350  0idnsgd  19137  pmtrprfv  19419  pmtrprfv3  19420  symggen  19436  pmtr3ncomlem1  19439  psgnunilem1  19459  lspprcl  20968  lsptpcl  20969  lspprss  20982  lspprid1  20987  lsppratlem2  21141  lsppratlem3  21142  lsppratlem4  21143  drngnidl  21236  drnglpir  21325  mdetralt  22591  topgele  22913  pptbas  22991  isconn2  23397  xpsdsval  24364  itgioo  25801  wilthlem2  27050  perfectlem2  27211  upgrex  29179  upgr1e  29200  uspgr1e  29331  eupth2lems  30326  s2f1  33024  pmtrcnel  33170  pmtrcnel2  33171  fzo0pmtrlast  33173  pmtridf1o  33175  cycpm2tr  33200  cyc3co2  33221  cyc3evpm  33231  cyc3genpmlem  33232  cyc3conja  33238  elrgspnsubrunlem1  33328  gsumind  33428  linds2eq  33464  drngmxidlr  33561  mplmulmvr  33723  esplylem  33750  esplympl  33751  esplyfv1  33753  esplyfval3  33756  esplyfvaln  33758  esplyind  33759  constrllcllem  33936  constrlccllem  33937  poimirlem9  37996  clsk1indlem4  44488  clsk1indlem1  44489  mnuprssd  44713  mnuprdlem4  44719  limsup10exlem  46215  meadjun  46905  clnbgrgrimlem  48424  stgredgiun  48449  stgrnbgr0  48455  grlimprclnbgrvtx  48490  grlimgrtrilem1  48492  gpgiedgdmellem  48537  gpgprismgriedgdmss  48543  line2  49243  line2y  49246  lubprlem  49452  joindm3  49459  meetdm3  49461  toplatjoin  49492  toplatmeet  49493