Theorem prssd 4755

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3936  {cpr 4569

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-sn 4568  df-pr 4570

This theorem is referenced by:  fpr2g  6974  f1prex  7040  fveqf1o  7058  fr3nr  7494  en2eqpr  9433  en2eleq  9434  r0weon  9438  wuncval2  10169  nehash2  13833  1idssfct  16024  basprssdmsets  16549  mrcun  16893  joinval2  17619  meetval2  17633  0idnsgd  18323  pmtrprfv  18581  pmtrprfv3  18582  symggen  18598  pmtr3ncomlem1  18601  psgnunilem1  18621  lspprcl  19750  lsptpcl  19751  lspprss  19764  lspprid1  19769  lsppratlem2  19920  lsppratlem3  19921  lsppratlem4  19922  drngnidl  20002  drnglpir  20026  mdetralt  21217  topgele  21538  pptbas  21616  isconn2  22022  xpsdsval  22991  itgioo  24416  wilthlem2  25646  perfectlem2  25806  upgrex  26877  upgr1e  26898  uspgr1e  27026  eupth2lems  28017  s2f1  30621  pmtrcnel  30733  pmtrcnel2  30734  pmtridf1o  30736  cycpm2tr  30761  cyc3co2  30782  cyc3evpm  30792  cyc3genpmlem  30793  cyc3conja  30799  linds2eq  30941  poimirlem9  34916  clsk1indlem4  40414  clsk1indlem1  40415  mnuprssd  40625  mnuprdlem4  40631  limsup10exlem  42073  meadjun  42764  line2  44759  line2y  44762