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

Theorem prssi 3890
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 3889 . 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 1717    C_ wss 3256   {cpr 3751
This theorem is referenced by:  prelpwi  4345  fr2nr  4494  fr3nr  4693  ordunel  4740  fveqf1o  5961  1sdom  7240  en2eqpr  7817  r0weon  7820  dfac2  7937  wuncval2  8548  tskpr  8571  m1expcl2  11323  m1expcl  11324  gcdcllem3  12933  1idssfct  13005  mreincl  13744  mrcun  13767  acsfn2  13808  joinval2  14366  meetval2  14373  ipole  14504  subrgin  15811  lssincl  15961  lspprcl  15974  lsptpcl  15975  lspprid1  15993  lspvadd  16088  lsppratlem2  16140  lsppratlem4  16142  unopn  16892  pptbas  16988  incld  17023  indiscld  17071  leordtval2  17191  iscon2  17391  xpsdsval  18312  ovolioo  19322  i1f1  19442  itgioo  19567  aannenlem2  20106  wilthlem2  20712  perfectlem2  20874  dchrisum0re  21067  umgraex  21218  umgra1  21221  uslgra1  21252  constr1trl  21429  constr2trl  21439  constr3trllem3  21480  eupath2  21543  umgrabi  21546  konigsberg  21550  sshjval3  22697  pr01ssre  24204  esumsn  24245  prsiga  24303  difelsiga  24305  measssd  24356  probun  24449  kur14lem1  24664  fprb  25146  ssoninhaus  25905  inidl  26324  en2eleq  27043  pmtrprfv  27058  symggen  27073  psgnunilem1  27078  cnmsgnbas  27097  cnmsgngrp  27098  frgra3vlem2  27747  4cycl2v2nb  27762  pmapmeet  29938  diameetN  31222  dihmeetcN  31468  dihmeet  31509  dvh4dimlem  31609  dvhdimlem  31610  dvh4dimN  31613  dvh3dim3N  31615  lcfrlem23  31731  lcfrlem25  31733  lcfrlem35  31743  mapdindp2  31887  lspindp5  31936
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-un 3261  df-in 3263  df-ss 3270  df-sn 3756  df-pr 3757
  Copyright terms: Public domain W3C validator