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

Theorem prssi 3946
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 3945 . 2  |-  ( ( A  e.  C  /\  B  e.  C )  ->  ( ( A  e.  C  /\  B  e.  C )  <->  { A ,  B }  C_  C
) )
21ibi 233 1  |-  ( ( A  e.  C  /\  B  e.  C )  ->  { A ,  B }  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725    C_ wss 3312   {cpr 3807
This theorem is referenced by:  tpssi  3957  prelpwi  4403  fr2nr  4552  fr3nr  4752  ordunel  4799  fveqf1o  6021  1sdom  7303  en2eqpr  7883  r0weon  7886  dfac2  8003  wuncval2  8614  tskpr  8637  m1expcl2  11395  m1expcl  11396  gcdcllem3  13005  1idssfct  13077  mreincl  13816  mrcun  13839  acsfn2  13880  joinval2  14438  meetval2  14445  ipole  14576  subrgin  15883  lssincl  16033  lspprcl  16046  lsptpcl  16047  lspprid1  16065  lspvadd  16160  lsppratlem2  16212  lsppratlem4  16214  unopn  16968  pptbas  17064  incld  17099  indiscld  17147  leordtval2  17268  iscon2  17469  xpsdsval  18403  ovolioo  19454  i1f1  19574  itgioo  19699  aannenlem2  20238  wilthlem2  20844  perfectlem2  21006  dchrisum0re  21199  umgraex  21350  umgra1  21353  uslgra1  21384  constr1trl  21580  constr3trllem3  21631  eupath2  21694  umgrabi  21697  konigsberg  21701  sshjval3  22848  pr01ssre  24407  esumsn  24448  prsiga  24506  difelsiga  24508  measssd  24561  probun  24669  kur14lem1  24884  fprb  25389  ssoninhaus  26190  inidl  26631  en2eleq  27349  pmtrprfv  27364  symggen  27379  psgnunilem1  27384  cnmsgnbas  27403  cnmsgngrp  27404  frgra3vlem2  28328  4cycl2v2nb  28343  pmapmeet  30507  diameetN  31791  dihmeetcN  32037  dihmeet  32078  dvh4dimlem  32178  dvhdimlem  32179  dvh4dimN  32182  dvh3dim3N  32184  lcfrlem23  32300  lcfrlem25  32302  lcfrlem35  32312  mapdindp2  32456  lspindp5  32505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-in 3319  df-ss 3326  df-sn 3812  df-pr 3813
  Copyright terms: Public domain W3C validator