Theorem prssd 4760

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3891  {cpr 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-in 3898  df-ss 3908  df-sn 4567  df-pr 4569

This theorem is referenced by:  fpr2g  7081  f1prex  7149  fveqf1o  7168  fr3nr  7613  en2eqpr  9747  en2eleq  9748  r0weon  9752  wuncval2  10487  nehash2  14169  1idssfct  16366  basprssdmsets  16906  mrcun  17312  joinval2  18080  meetval2  18094  0idnsgd  18780  pmtrprfv  19042  pmtrprfv3  19043  symggen  19059  pmtr3ncomlem1  19062  psgnunilem1  19082  lspprcl  20221  lsptpcl  20222  lspprss  20235  lspprid1  20240  lsppratlem2  20391  lsppratlem3  20392  lsppratlem4  20393  drngnidl  20481  drnglpir  20505  mdetralt  21738  topgele  22060  pptbas  22139  isconn2  22546  xpsdsval  23515  itgioo  24961  wilthlem2  26199  perfectlem2  26359  upgrex  27443  upgr1e  27464  uspgr1e  27592  eupth2lems  28581  s2f1  31198  pmtrcnel  31337  pmtrcnel2  31338  pmtridf1o  31340  cycpm2tr  31365  cyc3co2  31386  cyc3evpm  31396  cyc3genpmlem  31397  cyc3conja  31403  linds2eq  31554  poimirlem9  35765  clsk1indlem4  41607  clsk1indlem1  41608  mnuprssd  41840  mnuprdlem4  41846  limsup10exlem  43267  meadjun  43954  line2  46050  line2y  46053  lubprlem  46208  joindm3  46215  meetdm3  46217  toplatjoin  46240  toplatmeet  46241