Theorem prssd 4715

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528

This theorem is referenced by:  fpr2g  6951  f1prex  7018  fveqf1o  7037  fr3nr  7474  en2eqpr  9418  en2eleq  9419  r0weon  9423  wuncval2  10158  nehash2  13828  1idssfct  16014  basprssdmsets  16541  mrcun  16885  joinval2  17611  meetval2  17625  0idnsgd  18315  pmtrprfv  18573  pmtrprfv3  18574  symggen  18590  pmtr3ncomlem1  18593  psgnunilem1  18613  lspprcl  19743  lsptpcl  19744  lspprss  19757  lspprid1  19762  lsppratlem2  19913  lsppratlem3  19914  lsppratlem4  19915  drngnidl  19995  drnglpir  20019  mdetralt  21213  topgele  21535  pptbas  21613  isconn2  22019  xpsdsval  22988  itgioo  24419  wilthlem2  25654  perfectlem2  25814  upgrex  26885  upgr1e  26906  uspgr1e  27034  eupth2lems  28023  s2f1  30647  pmtrcnel  30783  pmtrcnel2  30784  pmtridf1o  30786  cycpm2tr  30811  cyc3co2  30832  cyc3evpm  30842  cyc3genpmlem  30843  cyc3conja  30849  linds2eq  30995  poimirlem9  35066  clsk1indlem4  40747  clsk1indlem1  40748  mnuprssd  40977  mnuprdlem4  40983  limsup10exlem  42414  meadjun  43101  line2  45166  line2y  45169