Theorem prssi 4167

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 4166	. 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 1802   C_ wss 3458   {cpr 4012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-un 3463  df-in 3465  df-ss 3472  df-sn 4011  df-pr 4013

This theorem is referenced by:  tpssi  4177  prelpwi  4680  fr2nr  4843  fveqf1o  6186  fr3nr  6596  ordunel  6643  1sdom  7720  en2eqpr  8383  en2eleq  8384  r0weon  8388  dfac2  8509  wuncval2  9123  tskpr  9146  m1expcl2  12162  m1expcl  12163  wrdlen2i  12858  gcdcllem3  14023  1idssfct  14095  mreincl  14868  mrcun  14891  acsfn2  14932  joinval2  15508  meetval2  15522  ipole  15657  pmtrprfv  16347  pmtrprfv3  16348  symggen  16364  pmtr3ncomlem1  16367  pmtr3ncom  16369  psgnunilem1  16387  subrgin  17320  lssincl  17479  lspprcl  17492  lsptpcl  17493  lspprid1  17511  lspvadd  17610  lsppratlem2  17662  lsppratlem4  17664  cnmsgnbas  18481  cnmsgngrp  18482  psgninv  18485  zrhpsgnmhm  18487  mdetralt  18977  mdetunilem7  18987  unopn  19279  pptbas  19375  incld  19410  indiscld  19458  leordtval2  19579  iscon2  19781  xpsdsval  20750  ovolioo  21844  i1f1  21963  itgioo  22088  aannenlem2  22590  wilthlem2  23208  perfectlem2  23370  dchrisum0re  23563  nehash2  23764  umgraex  24188  umgra1  24191  uslgra1  24237  constr1trl  24455  constr3trllem3  24517  nbhashuvtx1  24780  eupath2  24845  umgrabi  24848  konigsberg  24852  frgra3vlem2  24866  4cycl2v2nb  24881  sshjval3  26137  pr01ssre  27897  esumsn  27938  prsiga  27997  difelsiga  27999  measssd  28052  eulerpartlemgs2  28185  eulerpartlemn  28186  probun  28224  signswch  28384  signsvfn  28405  signlem0  28410  kur14lem1  28516  fprb  29171  ssoninhaus  29881  inidl  30395  ibliooicc  31656  fourierdlem51  31825  fourierdlem64  31838  fourierdlem102  31876  fourierdlem114  31888  mapprop  32643  zlmodzxzel  32652  zlmodzxzldeplem1  32811  pmapmeet  35199  diameetN  36485  dihmeetcN  36731  dihmeet  36772  dvh4dimlem  36872  dvhdimlem  36873  dvh4dimN  36876  dvh3dim3N  36878  lcfrlem23  36994  lcfrlem25  36996  lcfrlem35  37006  mapdindp2  37150  lspindp5  37199