Theorem prssi 4760

Description: A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)

Assertion

Ref	Expression
prssi	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

Proof of Theorem prssi

Step	Hyp	Ref	Expression
1		prssg 4758	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
2	1	ibi 267	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2104   ⊆ wss 3892  {cpr 4567

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-un 3897  df-in 3899  df-ss 3909  df-sn 4566  df-pr 4568

This theorem is referenced by:  prssd  4761  tpssi  4775  fr2nr  5578  fprb  7101  f1ofvswap  7210  ordunel  7706  rex2dom  9067  1sdomOLD  9070  dfac2b  9932  tskpr  10572  m1expcl2  13850  m1expcl  13851  wrdlen2i  14700  gcdcllem3  16253  lcmfpr  16377  mreincl  17353  acsfn2  17417  ipole  18297  pmtr3ncom  19128  subrgin  20092  lssincl  20272  lspvadd  20403  cnmsgnbas  20828  cnmsgngrp  20829  psgninv  20832  zrhpsgnmhm  20834  mdetunilem7  21812  unopn  22097  incld  22239  indiscld  22287  leordtval2  22408  ovolioo  24777  i1f1  24899  aannenlem2  25534  upgrbi  27508  umgrbi  27516  frgr3vlem2  28683  4cycl2v2nb  28698  sshjval3  29761  pr01ssre  31183  psgnid  31409  pmtrto1cl  31411  cnmsgn0g  31458  altgnsg  31461  mdetpmtr1  31818  mdetpmtr12  31820  esumsnf  32077  prsiga  32144  difelsiga  32146  measssd  32228  carsgsigalem  32327  carsgclctun  32333  pmeasmono  32336  eulerpartlemgs2  32392  eulerpartlemn  32393  probun  32431  signswch  32585  signsvfn  32606  signlem0  32611  breprexpnat  32659  kur14lem1  33213  ssoninhaus  34682  poimirlem15  35836  inidl  36232  pmapmeet  37829  diameetN  39112  dihmeetcN  39358  dihmeet  39399  dvh4dimlem  39499  dvhdimlem  39500  dvh4dimN  39503  dvh3dim3N  39505  lcfrlem23  39621  lcfrlem25  39623  lcfrlem35  39633  mapdindp2  39777  lspindp5  39826  brfvrcld  41337  corclrcl  41353  corcltrcl  41385  ibliooicc  43561  fourierdlem51  43747  fourierdlem64  43760  fourierdlem102  43798  fourierdlem114  43810  sge0sn  43967  ovnsubadd2lem  44233  sprvalpw  44990  prprvalpw  45025  perfectALTVlem2  45232  nnsum3primesgbe  45302  fprmappr  45739  zlmodzxzel  45749  zlmodzxzldeplem1  45899  2arymaptfo  46058  prelrrx2  46117  line2x  46158  line2y  46159  onsetreclem2  46469