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

Theorem prid2g 3981
Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
Assertion
Ref Expression
prid2g  |-  ( B  e.  V  ->  B  e.  { A ,  B } )

Proof of Theorem prid2g
StepHypRef Expression
1 prid1g 3980 . 2  |-  ( B  e.  V  ->  B  e.  { B ,  A } )
2 prcom 3952 . 2  |-  { B ,  A }  =  { A ,  B }
31, 2syl6eleq 2532 1  |-  ( B  e.  V  ->  B  e.  { A ,  B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   {cpr 3878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2973  df-un 3332  df-sn 3877  df-pr 3879
This theorem is referenced by:  unisn2  4427  fr2nr  4697  pw2f1olem  7414  gcdcllem3  13696  pmtrprfv  15958  m2detleib  18436  indistopon  18604  pptbas  18611  coseq0negpitopi  21964  usgra2edg  23300  nb3graprlem1  23358  nb3graprlem2  23359  2trllemF  23447  vdgr1b  23573  prsiga  26573  ftc1anclem8  28472  imarnf1pr  30148
  Copyright terms: Public domain W3C validator