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

Theorem prssi 3771
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 3770 . 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 1684    C_ wss 3152   {cpr 3641
This theorem is referenced by:  fr2nr  4371  fr3nr  4571  ordunel  4618  fveqf1o  5806  1sdom  7065  en2eqpr  7637  r0weon  7640  dfac2  7757  wuncval2  8369  tskpr  8392  m1expcl2  11125  m1expcl  11126  gcdcllem3  12692  1idssfct  12764  mreincl  13501  mrcun  13524  acsfn2  13565  isdrs2  14073  joinval2  14123  meetval2  14130  ipole  14261  subrgin  15568  lssincl  15722  lspprcl  15735  lsptpcl  15736  lspprid1  15754  lspvadd  15849  lsppratlem2  15901  lsppratlem4  15903  unopn  16649  pptbas  16745  incld  16780  indiscld  16828  leordtval2  16942  iscon2  17140  xpsdsval  17945  ovolioo  18925  i1f1  19045  itgioo  19170  aannenlem2  19709  wilthlem2  20307  perfectlem2  20469  dchrisum0re  20662  sshjval3  21933  prelpwi  23185  esumsn  23437  prsiga  23492  difelsiga  23494  unelsiga  23495  measssd  23543  pr01ssre  23601  probun  23622  kur14lem1  23737  umgraex  23875  umgra1  23878  eupath2  23904  umgrabi  23907  konigsberg  23911  fprb  24129  ssoninhaus  24887  inidl  26655  en2eleq  27381  pmtrprfv  27396  symggen  27411  psgnunilem1  27416  cnmsgnbas  27435  cnmsgngrp  27436  prelpw  28074  uslgra1  28118  usgra1  28119  frgra3vlem2  28179  pmapmeet  29962  diameetN  31246  dihmeetcN  31492  dihmeet  31533  dvh4dimlem  31633  dvhdimlem  31634  dvh4dimN  31637  dvh3dim3N  31639  lcfrlem23  31755  lcfrlem25  31757  lcfrlem35  31767  mapdindp2  31911  lspindp5  31960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator