Theorem prssd 4783

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587

This theorem is used by:  fpr2g  7211  f1prex  7286  fveqf1o  7304  fr3nr  7772  en2eqpr  10013  en2eleq  10014  r0weon  10018  wuncval2  10759  nehash2  14542  1idssfct  16773  basprssdmsets  17316  mrcun  17713  joinval2  18470  meetval2  18484  0idnsgd  19297  pmtrprfv  19583  pmtrprfv3  19584  symggen  19600  pmtr3ncomlem1  19603  psgnunilem1  19623  lspprcl  21165  lsptpcl  21166  lspprss  21179  lspprid1  21184  lsppratlem2  21338  lsppratlem3  21339  lsppratlem4  21340  drngnidl  21443  drnglpir  21566  mdetralt  22833  topgele  23158  pptbas  23236  isconn2  23642  xpsdsval  24610  itgioo  26046  wilthlem2  27308  perfectlem2  27469  upgrex  29552  upgr1e  29573  uspgr1e  29707  eupth2lems  30721  s2f1  33392  pmtrcnel  33532  pmtrcnel2  33533  fzo0pmtrlast  33535  pmtridf1o  33537  cycpm2tr  33562  cyc3co2  33583  cyc3evpm  33593  cyc3genpmlem  33594  cyc3conja  33600  elrgspnsubrunlem1  33690  gsumind  33788  linds2eq  33817  drngmxidlr  33883  mplmulmvr  34052  esplylem  34079  esplympl  34080  esplyfv1  34082  esplyfval3  34085  esplyfvaln  34087  esplyind  34088  constrllcllem  34265  constrlccllem  34266  poimirlem9  38381  clsk1indlem4  44887  clsk1indlem1  44888  mnuprssd  45096  mnuprdlem4  45102  limsup10exlem  46603  meadjun  47293  clnbgrgrimlem  48852  stgredgiun  48877  stgrnbgr0  48883  grlimprclnbgrvtx  48918  grlimgrtrilem1  48920  gpgiedgdmellem  48965  gpgprismgriedgdmss  48971  line2  49685  line2y  49688  lubprlem  49891  joindm3  49898  meetdm3  49900  toplatjoin  49931  toplatmeet  49932