Theorem prssi 4027

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 4026	. 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 1756   C_ wss 3326   {cpr 3877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-un 3331  df-in 3333  df-ss 3340  df-sn 3876  df-pr 3878

This theorem is referenced by:  tpssi  4037  prelpwi  4537  fr2nr  4696  fveqf1o  5998  fr3nr  6389  ordunel  6436  1sdom  7513  en2eqpr  8172  en2eleq  8173  r0weon  8177  dfac2  8298  wuncval2  8912  tskpr  8935  m1expcl2  11885  m1expcl  11886  wrdlen2i  12544  gcdcllem3  13695  1idssfct  13767  mreincl  14535  mrcun  14558  acsfn2  14599  joinval2  15177  meetval2  15191  ipole  15326  pmtrprfv  15957  pmtrprfv3  15958  symggen  15974  pmtr3ncomlem1  15977  pmtr3ncom  15979  psgnunilem1  15997  subrgin  16886  lssincl  17044  lspprcl  17057  lsptpcl  17058  lspprid1  17076  lspvadd  17175  lsppratlem2  17227  lsppratlem4  17229  cnmsgnbas  18006  cnmsgngrp  18007  psgninv  18010  zrhpsgnmhm  18012  mdetralt  18412  mdetunilem7  18422  unopn  18514  pptbas  18610  incld  18645  indiscld  18693  leordtval2  18814  iscon2  19016  xpsdsval  19954  ovolioo  21047  i1f1  21166  itgioo  21291  aannenlem2  21793  wilthlem2  22405  perfectlem2  22567  dchrisum0re  22760  nehash2  22958  umgraex  23255  umgra1  23258  uslgra1  23289  constr1trl  23485  constr3trllem3  23536  eupath2  23599  umgrabi  23602  konigsberg  23606  sshjval3  24755  pr01ssre  26472  esumsn  26513  prsiga  26572  difelsiga  26574  measssd  26627  eulerpartlemgs2  26761  eulerpartlemn  26762  probun  26800  signswch  26960  signsvfn  26981  signlem0  26986  kur14lem1  27092  fprb  27582  ssoninhaus  28292  inidl  28827  nbhashuvtx1  30530  frgra3vlem2  30590  4cycl2v2nb  30605  mapprop  30733  zlmodzxzel  30749  zlmodzxzldeplem1  31039  pmapmeet  33414  diameetN  34698  dihmeetcN  34944  dihmeet  34985  dvh4dimlem  35085  dvhdimlem  35086  dvh4dimN  35089  dvh3dim3N  35091  lcfrlem23  35207  lcfrlem25  35209  lcfrlem35  35219  mapdindp2  35363  lspindp5  35412