Theorem prssi 4141

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 4140	. 2 |- ( ( A e. C /\ B e. C ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) )
2	1	ibi 249	1 |- ( ( A e. C /\ B e. C ) -> { A , B } C_ C )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1898   C_ wss 3416   {cpr 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-in 3423  df-ss 3430  df-sn 3981  df-pr 3983

This theorem is referenced by:  tpssi  4151  prelpwi  4664  fr2nr  4834  f1prex  6212  fveqf1o  6230  fr3nr  6638  ordunel  6686  1sdom  7806  en2eqpr  8469  en2eleq  8470  r0weon  8474  dfac2  8592  wuncval2  9203  tskpr  9226  m1expcl2  12332  m1expcl  12333  wrdlen2i  13073  gcdcllem3  14530  lcmfpr  14655  1idssfct  14685  mreincl  15560  mrcun  15583  acsfn2  15624  joinval2  16310  meetval2  16324  ipole  16459  pmtrprfv  17149  pmtrprfv3  17150  symggen  17166  pmtr3ncomlem1  17169  pmtr3ncom  17171  psgnunilem1  17189  subrgin  18086  lssincl  18243  lspprcl  18256  lsptpcl  18257  lspprid1  18275  lspvadd  18374  lsppratlem2  18426  lsppratlem4  18428  cnmsgnbas  19201  cnmsgngrp  19202  psgninv  19205  zrhpsgnmhm  19207  mdetralt  19688  mdetunilem7  19698  unopn  19988  pptbas  20078  incld  20113  indiscld  20162  leordtval2  20283  iscon2  20484  xpsdsval  21451  ovolioo  22577  i1f1  22704  itgioo  22829  aannenlem2  23341  wilthlem2  24050  perfectlem2  24214  dchrisum0re  24407  nehash2  24608  umgraex  25106  umgra1  25109  uslgra1  25155  constr1trl  25374  constr3trllem3  25436  nbhashuvtx1  25699  eupath2  25764  umgrabi  25767  konigsberg  25771  frgra3vlem2  25785  4cycl2v2nb  25800  sshjval3  27063  psgnid  28661  pmtrto1cl  28663  mdetpmtr1  28700  mdetpmtr12  28702  pr01ssre  28890  esumsnf  28936  prsiga  29004  difelsiga  29006  inelpisys  29027  measssd  29088  carsgsigalem  29197  carsgclctun  29203  pmeasmono  29207  eulerpartlemgs2  29263  eulerpartlemn  29264  probun  29302  signswch  29500  signsvfn  29521  signlem0  29526  kur14lem1  29979  fprb  30463  ssoninhaus  31158  poimirlem9  31995  poimirlem15  32001  inidl  32309  pmapmeet  33384  diameetN  34670  dihmeetcN  34916  dihmeet  34957  dvh4dimlem  35057  dvhdimlem  35058  dvh4dimN  35061  dvh3dim3N  35063  lcfrlem23  35179  lcfrlem25  35181  lcfrlem35  35191  mapdindp2  35335  lspindp5  35384  brfvrcld  36329  corclrcl  36345  corcltrcl  36377  ibliooicc  37934  fourierdlem51  38122  fourierdlem64  38135  fourierdlem102  38173  fourierdlem114  38185  sge0sn  38324  ovnsubadd2lem  38574  perfectALTVlem2  38979  nnsum3primesgbe  39022  upgrex  39327  upgr1e  39345  uspgr1e  39465  mapprop  40496  zlmodzxzel  40505  zlmodzxzldeplem1  40662