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

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

Proof of Theorem prid1g
StepHypRef Expression
1 eqid 2467 . . 3  |-  A  =  A
21orci 390 . 2  |-  ( A  =  A  \/  A  =  B )
3 elprg 4043 . 2  |-  ( A  e.  V  ->  ( A  e.  { A ,  B }  <->  ( A  =  A  \/  A  =  B ) ) )
42, 3mpbiri 233 1  |-  ( A  e.  V  ->  A  e.  { A ,  B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    = wceq 1379    e. wcel 1767   {cpr 4029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030
This theorem is referenced by:  prid2g  4134  prid1  4135  opth1  4720  fr2nr  4857  fveqf1o  6193  pw2f1olem  7621  gcdcllem3  14010  pmtrprfv  16284  pptbas  19303  coseq0negpitopi  22657  usgra2edg  24086  nbgraf1olem1  24145  nbgraf1olem3  24147  nbgraf1olem5  24149  nb3graprlem1  24155  nb3graprlem2  24156  constr1trl  24294  vdgr1b  24608  vdusgra0nedg  24612  usgravd0nedg  24622  vdn0frgrav2  24728  vdgn0frgrav2  24729  ftc1anclem8  29702  kelac2  30643  fourierdlem54  31489  imarnf1pr  31804  usgvad2edg  31906
  Copyright terms: Public domain W3C validator