Theorem prssd 4773

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3903  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920  df-sn 4578  df-pr 4580

This theorem is referenced by:  fpr2g  7147  f1prex  7221  fveqf1o  7239  fr3nr  7708  en2eqpr  9901  en2eleq  9902  r0weon  9906  wuncval2  10641  nehash2  14381  1idssfct  16591  basprssdmsets  17132  mrcun  17528  joinval2  18285  meetval2  18299  0idnsgd  19050  pmtrprfv  19332  pmtrprfv3  19333  symggen  19349  pmtr3ncomlem1  19352  psgnunilem1  19372  lspprcl  20881  lsptpcl  20882  lspprss  20895  lspprid1  20900  lsppratlem2  21055  lsppratlem3  21056  lsppratlem4  21057  drngnidl  21150  drnglpir  21239  mdetralt  22493  topgele  22815  pptbas  22893  isconn2  23299  xpsdsval  24267  itgioo  25715  wilthlem2  26977  perfectlem2  27139  upgrex  29037  upgr1e  29058  uspgr1e  29189  eupth2lems  30182  s2f1  32886  pmtrcnel  33031  pmtrcnel2  33032  fzo0pmtrlast  33034  pmtridf1o  33036  cycpm2tr  33061  cyc3co2  33082  cyc3evpm  33092  cyc3genpmlem  33093  cyc3conja  33099  elrgspnsubrunlem1  33187  linds2eq  33318  drngmxidlr  33415  constrllcllem  33719  constrlccllem  33720  poimirlem9  37613  clsk1indlem4  44021  clsk1indlem1  44022  mnuprssd  44246  mnuprdlem4  44252  limsup10exlem  45757  meadjun  46447  clnbgrgrimlem  47921  stgredgiun  47946  stgrnbgr0  47952  grlimprclnbgrvtx  47987  grlimgrtrilem1  47989  gpgiedgdmellem  48034  gpgprismgriedgdmss  48040  line2  48741  line2y  48744  lubprlem  48950  joindm3  48957  meetdm3  48959  toplatjoin  48990  toplatmeet  48991