MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prssi Unicode version

Theorem prssi 4186
Description: A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
Assertion
Ref Expression
prssi

Proof of Theorem prssi
StepHypRef Expression
1 prssg 4185 . 2
21ibi 241 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  C_wss 3475  {cpr 4031
This theorem is referenced by:  tpssi  4196  prelpwi  4699  fr2nr  4862  fveqf1o  6205  fr3nr  6615  ordunel  6662  1sdom  7742  en2eqpr  8406  en2eleq  8407  r0weon  8411  dfac2  8532  wuncval2  9146  tskpr  9169  m1expcl2  12188  m1expcl  12189  wrdlen2i  12884  gcdcllem3  14151  1idssfct  14223  mreincl  14996  mrcun  15019  acsfn2  15060  joinval2  15639  meetval2  15653  ipole  15788  pmtrprfv  16478  pmtrprfv3  16479  symggen  16495  pmtr3ncomlem1  16498  pmtr3ncom  16500  psgnunilem1  16518  subrgin  17452  lssincl  17611  lspprcl  17624  lsptpcl  17625  lspprid1  17643  lspvadd  17742  lsppratlem2  17794  lsppratlem4  17796  cnmsgnbas  18614  cnmsgngrp  18615  psgninv  18618  zrhpsgnmhm  18620  mdetralt  19110  mdetunilem7  19120  unopn  19412  pptbas  19509  incld  19544  indiscld  19592  leordtval2  19713  iscon2  19915  xpsdsval  20884  ovolioo  21978  i1f1  22097  itgioo  22222  aannenlem2  22725  wilthlem2  23343  perfectlem2  23505  dchrisum0re  23698  nehash2  23899  umgraex  24323  umgra1  24326  uslgra1  24372  constr1trl  24590  constr3trllem3  24652  nbhashuvtx1  24915  eupath2  24980  umgrabi  24983  konigsberg  24987  frgra3vlem2  25001  4cycl2v2nb  25016  sshjval3  26272  pr01ssre  28031  esumsn  28072  prsiga  28131  difelsiga  28133  measssd  28186  eulerpartlemgs2  28319  eulerpartlemn  28320  probun  28358  signswch  28518  signsvfn  28539  signlem0  28544  kur14lem1  28650  fprb  29203  ssoninhaus  29913  inidl  30427  ibliooicc  31770  fourierdlem51  31940  fourierdlem64  31953  fourierdlem102  31991  fourierdlem114  32003  mapprop  32935  zlmodzxzel  32944  zlmodzxzldeplem1  33101  pmapmeet  35497  diameetN  36783  dihmeetcN  37029  dihmeet  37070  dvh4dimlem  37170  dvhdimlem  37171  dvh4dimN  37174  dvh3dim3N  37176  lcfrlem23  37292  lcfrlem25  37294  lcfrlem35  37304  mapdindp2  37448  lspindp5  37497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-sn 4030  df-pr 4032
  Copyright terms: Public domain W3C validator