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

Theorem prid2g 4123
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 4122 . 2  |-  ( B  e.  V  ->  B  e.  { B ,  A } )
2 prcom 4094 . 2  |-  { B ,  A }  =  { A ,  B }
31, 2syl6eleq 2552 1  |-  ( B  e.  V  ->  B  e.  { A ,  B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   {cpr 4018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-sn 4017  df-pr 4019
This theorem is referenced by:  unisn2  4573  fr2nr  4846  pw2f1olem  7614  hashprdifel  12447  gcdcllem3  14235  mgm2nsgrplem1  16235  mgm2nsgrplem2  16236  mgm2nsgrplem3  16237  sgrp2nmndlem1  16240  sgrp2rid2  16243  pmtrprfv  16677  m2detleib  19300  indistopon  19669  pptbas  19676  coseq0negpitopi  23062  usgra2edg  24584  nb3graprlem1  24653  nb3graprlem2  24654  2trllemF  24753  vdgr1b  25106  prsiga  28361  ftc1anclem8  30337  fourierdlem54  32182  imarnf1pr  32683  usgvad2edg  32783
  Copyright terms: Public domain W3C validator