Theorem prssi 4176

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1762   C_ wss 3469   {cpr 4022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474  df-in 3476  df-ss 3483  df-sn 4021  df-pr 4023

This theorem is referenced by:  tpssi  4186  prelpwi  4687  fr2nr  4850  fveqf1o  6184  fr3nr  6586  ordunel  6633  1sdom  7712  en2eqpr  8374  en2eleq  8375  r0weon  8379  dfac2  8500  wuncval2  9114  tskpr  9137  m1expcl2  12144  m1expcl  12145  wrdlen2i  12834  gcdcllem3  13999  1idssfct  14071  mreincl  14843  mrcun  14866  acsfn2  14907  joinval2  15485  meetval2  15499  ipole  15634  pmtrprfv  16267  pmtrprfv3  16268  symggen  16284  pmtr3ncomlem1  16287  pmtr3ncom  16289  psgnunilem1  16307  subrgin  17228  lssincl  17387  lspprcl  17400  lsptpcl  17401  lspprid1  17419  lspvadd  17518  lsppratlem2  17570  lsppratlem4  17572  cnmsgnbas  18374  cnmsgngrp  18375  psgninv  18378  zrhpsgnmhm  18380  mdetralt  18870  mdetunilem7  18880  unopn  19172  pptbas  19268  incld  19303  indiscld  19351  leordtval2  19472  iscon2  19674  xpsdsval  20612  ovolioo  21706  i1f1  21825  itgioo  21950  aannenlem2  22452  wilthlem2  23064  perfectlem2  23226  dchrisum0re  23419  nehash2  23620  umgraex  23986  umgra1  23989  uslgra1  24034  constr1trl  24252  constr3trllem3  24314  nbhashuvtx1  24577  eupath2  24642  umgrabi  24645  konigsberg  24649  frgra3vlem2  24663  4cycl2v2nb  24678  sshjval3  25934  pr01ssre  27657  esumsn  27698  prsiga  27757  difelsiga  27759  measssd  27812  eulerpartlemgs2  27945  eulerpartlemn  27946  probun  27984  signswch  28144  signsvfn  28165  signlem0  28170  kur14lem1  28276  fprb  28766  ssoninhaus  29476  inidl  30017  ibliooicc  31244  fourierdlem51  31413  fourierdlem64  31426  fourierdlem93  31455  fourierdlem102  31464  fourierdlem114  31476  mapprop  31874  zlmodzxzel  31883  zlmodzxzldeplem1  32057  pmapmeet  34444  diameetN  35728  dihmeetcN  35974  dihmeet  36015  dvh4dimlem  36115  dvhdimlem  36116  dvh4dimN  36119  dvh3dim3N  36121  lcfrlem23  36237  lcfrlem25  36239  lcfrlem35  36249  mapdindp2  36393  lspindp5  36442