Theorem prssd 4778

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901  {cpr 4582

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-sn 4581  df-pr 4583

This theorem is referenced by:  fpr2g  7157  f1prex  7230  fveqf1o  7248  fr3nr  7717  en2eqpr  9917  en2eleq  9918  r0weon  9922  wuncval2  10658  nehash2  14397  1idssfct  16607  basprssdmsets  17148  mrcun  17545  joinval2  18302  meetval2  18316  0idnsgd  19100  pmtrprfv  19382  pmtrprfv3  19383  symggen  19399  pmtr3ncomlem1  19402  psgnunilem1  19422  lspprcl  20929  lsptpcl  20930  lspprss  20943  lspprid1  20948  lsppratlem2  21103  lsppratlem3  21104  lsppratlem4  21105  drngnidl  21198  drnglpir  21287  mdetralt  22552  topgele  22874  pptbas  22952  isconn2  23358  xpsdsval  24325  itgioo  25773  wilthlem2  27035  perfectlem2  27197  upgrex  29165  upgr1e  29186  uspgr1e  29317  eupth2lems  30313  s2f1  33027  pmtrcnel  33171  pmtrcnel2  33172  fzo0pmtrlast  33174  pmtridf1o  33176  cycpm2tr  33201  cyc3co2  33222  cyc3evpm  33232  cyc3genpmlem  33233  cyc3conja  33239  elrgspnsubrunlem1  33329  gsumind  33426  linds2eq  33462  drngmxidlr  33559  mplmulmvr  33704  esplylem  33724  esplympl  33725  esplyfv1  33727  esplyfval3  33730  esplyind  33731  constrllcllem  33909  constrlccllem  33910  poimirlem9  37830  clsk1indlem4  44295  clsk1indlem1  44296  mnuprssd  44520  mnuprdlem4  44526  limsup10exlem  46026  meadjun  46716  clnbgrgrimlem  48189  stgredgiun  48214  stgrnbgr0  48220  grlimprclnbgrvtx  48255  grlimgrtrilem1  48257  gpgiedgdmellem  48302  gpgprismgriedgdmss  48308  line2  49008  line2y  49011  lubprlem  49217  joindm3  49224  meetdm3  49226  toplatjoin  49257  toplatmeet  49258