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

Theorem prssi 3787
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
StepHypRef Expression
1 prssg 3786 . 2  |-  ( ( A  e.  C  /\  B  e.  C )  ->  ( ( A  e.  C  /\  B  e.  C )  <->  { A ,  B }  C_  C
) )
21ibi 232 1  |-  ( ( A  e.  C  /\  B  e.  C )  ->  { A ,  B }  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696    C_ wss 3165   {cpr 3654
This theorem is referenced by:  fr2nr  4387  fr3nr  4587  ordunel  4634  fveqf1o  5822  1sdom  7081  en2eqpr  7653  r0weon  7656  dfac2  7773  wuncval2  8385  tskpr  8408  m1expcl2  11141  m1expcl  11142  gcdcllem3  12708  1idssfct  12780  mreincl  13517  mrcun  13540  acsfn2  13581  isdrs2  14089  joinval2  14139  meetval2  14146  ipole  14277  subrgin  15584  lssincl  15738  lspprcl  15751  lsptpcl  15752  lspprid1  15770  lspvadd  15865  lsppratlem2  15917  lsppratlem4  15919  unopn  16665  pptbas  16761  incld  16796  indiscld  16844  leordtval2  16958  iscon2  17156  xpsdsval  17961  ovolioo  18941  i1f1  19061  itgioo  19186  aannenlem2  19725  wilthlem2  20323  perfectlem2  20485  dchrisum0re  20678  sshjval3  21949  prelpwi  23201  esumsn  23452  prsiga  23507  difelsiga  23509  unelsiga  23510  measssd  23558  pr01ssre  23616  probun  23637  kur14lem1  23752  umgraex  23890  umgra1  23893  eupath2  23919  umgrabi  23922  konigsberg  23926  fprb  24200  ssoninhaus  24959  inidl  26758  en2eleq  27484  pmtrprfv  27499  symggen  27514  psgnunilem1  27519  cnmsgnbas  27538  cnmsgngrp  27539  prelpw  28184  uslgra1  28252  usgra1  28253  constr3trllem3  28398  frgra3vlem2  28425  4cycl2v2nb  28438  pmapmeet  30584  diameetN  31868  dihmeetcN  32114  dihmeet  32155  dvh4dimlem  32255  dvhdimlem  32256  dvh4dimN  32259  dvh3dim3N  32261  lcfrlem23  32377  lcfrlem25  32379  lcfrlem35  32389  mapdindp2  32533  lspindp5  32582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator