Theorem prssi 4153

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

Assertion

Ref	Expression
prssi	|- ( ( A e. C /\ B e. C ) -> { A , B } C_ C )

Proof of Theorem prssi

Step	Hyp	Ref	Expression
1		prssg 4152	. 2 |- ( ( A e. C /\ B e. C ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) )
2	1	ibi 244	1 |- ( ( A e. C /\ B e. C ) -> { A , B } C_ C )

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1868   C_ wss 3436   {cpr 3998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-un 3441  df-in 3443  df-ss 3450  df-sn 3997  df-pr 3999

This theorem is referenced by:  tpssi  4163  prelpwi  4664  fr2nr  4827  f1prex  6193  fveqf1o  6211  fr3nr  6616  ordunel  6664  1sdom  7777  en2eqpr  8439  en2eleq  8440  r0weon  8444  dfac2  8561  wuncval2  9172  tskpr  9195  m1expcl2  12293  m1expcl  12294  wrdlen2i  13007  gcdcllem3  14460  lcmfpr  14585  1idssfct  14615  mreincl  15490  mrcun  15513  acsfn2  15554  joinval2  16240  meetval2  16254  ipole  16389  pmtrprfv  17079  pmtrprfv3  17080  symggen  17096  pmtr3ncomlem1  17099  pmtr3ncom  17101  psgnunilem1  17119  subrgin  18016  lssincl  18173  lspprcl  18186  lsptpcl  18187  lspprid1  18205  lspvadd  18304  lsppratlem2  18356  lsppratlem4  18358  cnmsgnbas  19130  cnmsgngrp  19131  psgninv  19134  zrhpsgnmhm  19136  mdetralt  19617  mdetunilem7  19627  unopn  19917  pptbas  20007  incld  20042  indiscld  20091  leordtval2  20212  iscon2  20413  xpsdsval  21380  ovolioo  22505  i1f1  22632  itgioo  22757  aannenlem2  23269  wilthlem2  23978  perfectlem2  24142  dchrisum0re  24335  nehash2  24536  umgraex  25034  umgra1  25037  uslgra1  25083  constr1trl  25301  constr3trllem3  25363  nbhashuvtx1  25626  eupath2  25691  umgrabi  25694  konigsberg  25698  frgra3vlem2  25712  4cycl2v2nb  25727  sshjval3  26990  psgnid  28603  pmtrto1cl  28605  mdetpmtr1  28642  mdetpmtr12  28644  pr01ssre  28832  esumsnf  28878  prsiga  28946  difelsiga  28948  inelpisys  28969  measssd  29030  carsgsigalem  29140  carsgclctun  29146  pmeasmono  29150  eulerpartlemgs2  29206  eulerpartlemn  29207  probun  29245  signswch  29443  signsvfn  29464  signlem0  29469  kur14lem1  29922  fprb  30405  ssoninhaus  31098  poimirlem9  31860  poimirlem15  31866  inidl  32174  pmapmeet  33254  diameetN  34540  dihmeetcN  34786  dihmeet  34827  dvh4dimlem  34927  dvhdimlem  34928  dvh4dimN  34931  dvh3dim3N  34933  lcfrlem23  35049  lcfrlem25  35051  lcfrlem35  35061  mapdindp2  35205  lspindp5  35254  brfvrcld  36140  corclrcl  36156  corcltrcl  36188  ibliooicc  37665  fourierdlem51  37838  fourierdlem64  37851  fourierdlem102  37889  fourierdlem114  37901  sge0sn  38006  perfectALTVlem2  38553  nnsum3primesgbe  38596  umgrex  38837  umgr1  38841  mapprop  39315  zlmodzxzel  39324  zlmodzxzldeplem1  39481