Theorem prssd 4767

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3897  {cpr 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-un 3902  df-in 3904  df-ss 3914  df-sn 4572  df-pr 4574

This theorem is referenced by:  fpr2g  7127  f1prex  7196  fveqf1o  7215  fr3nr  7664  en2eqpr  9843  en2eleq  9844  r0weon  9848  wuncval2  10583  nehash2  14267  1idssfct  16462  basprssdmsets  17002  mrcun  17408  joinval2  18176  meetval2  18190  0idnsgd  18875  pmtrprfv  19137  pmtrprfv3  19138  symggen  19154  pmtr3ncomlem1  19157  psgnunilem1  19177  lspprcl  20323  lsptpcl  20324  lspprss  20337  lspprid1  20342  lsppratlem2  20493  lsppratlem3  20494  lsppratlem4  20495  drngnidl  20583  drnglpir  20607  mdetralt  21840  topgele  22162  pptbas  22241  isconn2  22648  xpsdsval  23617  itgioo  25063  wilthlem2  26301  perfectlem2  26461  upgrex  27598  upgr1e  27619  uspgr1e  27747  eupth2lems  28738  s2f1  31354  pmtrcnel  31493  pmtrcnel2  31494  pmtridf1o  31496  cycpm2tr  31521  cyc3co2  31542  cyc3evpm  31552  cyc3genpmlem  31553  cyc3conja  31559  linds2eq  31714  poimirlem9  35858  clsk1indlem4  41888  clsk1indlem1  41889  mnuprssd  42121  mnuprdlem4  42127  limsup10exlem  43563  meadjun  44251  line2  46363  line2y  46366  lubprlem  46521  joindm3  46528  meetdm3  46530  toplatjoin  46553  toplatmeet  46554