Theorem prssi 4583

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 4581	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
2	1	ibi 259	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107   ⊆ wss 3792  {cpr 4400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797  df-in 3799  df-ss 3806  df-sn 4399  df-pr 4401

This theorem is referenced by:  prssd  4584  tpssi  4598  fr2nr  5333  fprb  6731  ordunel  7305  1sdom  8451  dfac2b  9286  dfac2OLD  9288  tskpr  9927  m1expcl2  13200  m1expcl  13201  wrdlen2i  14093  gcdcllem3  15629  lcmfpr  15746  mreincl  16645  acsfn2  16709  ipole  17544  pmtr3ncom  18278  subrgin  19195  lssincl  19360  lspprcl  19373  lsptpcl  19374  lspprid1  19392  lspvadd  19491  lsppratlem2  19545  lsppratlem4  19547  cnmsgnbas  20319  cnmsgngrp  20320  psgninv  20323  zrhpsgnmhm  20325  mdetralt  20819  mdetunilem7  20829  unopn  21115  pptbas  21220  incld  21255  indiscld  21303  leordtval2  21424  isconn2  21626  xpsdsval  22594  ovolioo  23772  i1f1  23894  itgioo  24019  aannenlem2  24521  wilthlem2  25247  perfectlem2  25407  upgrbi  26441  umgrbi  26449  frgr3vlem2  27682  4cycl2v2nb  27697  sshjval3  28785  pr01ssre  30134  psgnid  30445  pmtrto1cl  30447  mdetpmtr1  30487  mdetpmtr12  30489  esumsnf  30724  prsiga  30792  difelsiga  30794  inelpisys  30815  measssd  30876  carsgsigalem  30975  carsgclctun  30981  pmeasmono  30984  eulerpartlemgs2  31040  eulerpartlemn  31041  probun  31080  signswch  31238  signsvfn  31261  signlem0  31266  breprexpnat  31314  kur14lem1  31787  ssoninhaus  33030  lindsadd  34030  poimirlem15  34052  inidl  34455  pmapmeet  35929  diameetN  37212  dihmeetcN  37458  dihmeet  37499  dvh4dimlem  37599  dvhdimlem  37600  dvh4dimN  37603  dvh3dim3N  37605  lcfrlem23  37721  lcfrlem25  37723  lcfrlem35  37733  mapdindp2  37877  lspindp5  37926  brfvrcld  38944  corclrcl  38960  corcltrcl  38992  ibliooicc  41118  fourierdlem51  41305  fourierdlem64  41318  fourierdlem102  41356  fourierdlem114  41368  sge0sn  41524  ovnsubadd2lem  41790  sprvalpw  42423  prprvalpw  42458  perfectALTVlem2  42660  nnsum3primesgbe  42709  mapprop  43143  zlmodzxzel  43152  zlmodzxzldeplem1  43308  prelrrx2  43453  line2x  43494  line2y  43495  onsetreclem2  43561