Theorem prssi 4353

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

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   C_ wss 3574   {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-sn 4178  df-pr 4180

This theorem is referenced by:  prssd  4354  tpssi  4369  fr2nr  5092  f1prex  6539  fveqf1o  6557  fr3nr  6979  ordunel  7027  1sdom  8163  en2eqpr  8830  en2eleq  8831  r0weon  8835  dfac2  8953  wuncval2  9569  tskpr  9592  m1expcl2  12882  m1expcl  12883  wrdlen2i  13686  gcdcllem3  15223  lcmfpr  15340  1idssfct  15393  mreincl  16259  mrcun  16282  acsfn2  16324  joinval2  17009  meetval2  17023  ipole  17158  pmtrprfv  17873  pmtrprfv3  17874  symggen  17890  pmtr3ncomlem1  17893  pmtr3ncom  17895  psgnunilem1  17913  subrgin  18803  lssincl  18965  lspprcl  18978  lsptpcl  18979  lspprid1  18997  lspvadd  19096  lsppratlem2  19148  lsppratlem4  19150  cnmsgnbas  19924  cnmsgngrp  19925  psgninv  19928  zrhpsgnmhm  19930  mdetralt  20414  mdetunilem7  20424  unopn  20708  pptbas  20812  incld  20847  indiscld  20895  leordtval2  21016  isconn2  21217  xpsdsval  22186  ovolioo  23336  i1f1  23457  itgioo  23582  aannenlem2  24084  wilthlem2  24795  perfectlem2  24955  upgrbi  25988  umgrbi  25996  frgr3vlem2  27138  4cycl2v2nb  27153  sshjval3  28213  pr01ssre  29570  psgnid  29847  pmtrto1cl  29849  mdetpmtr1  29889  mdetpmtr12  29891  esumsnf  30126  prsiga  30194  difelsiga  30196  inelpisys  30217  measssd  30278  carsgsigalem  30377  carsgclctun  30383  pmeasmono  30386  eulerpartlemgs2  30442  eulerpartlemn  30443  probun  30481  signswch  30638  signsvfn  30659  signlem0  30664  breprexpnat  30712  kur14lem1  31188  fprb  31669  ssoninhaus  32447  poimirlem15  33424  inidl  33829  pmapmeet  35059  diameetN  36345  dihmeetcN  36591  dihmeet  36632  dvh4dimlem  36732  dvhdimlem  36733  dvh4dimN  36736  dvh3dim3N  36738  lcfrlem23  36854  lcfrlem25  36856  lcfrlem35  36866  mapdindp2  37010  lspindp5  37059  brfvrcld  37983  corclrcl  37999  corcltrcl  38031  ibliooicc  40187  fourierdlem51  40374  fourierdlem64  40387  fourierdlem102  40425  fourierdlem114  40437  sge0sn  40596  ovnsubadd2lem  40859  perfectALTVlem2  41631  nnsum3primesgbe  41680  sprvalpw  41730  mapprop  42124  zlmodzxzel  42133  zlmodzxzldeplem1  42289  onsetreclem2  42449