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

Theorem prid1g 3733
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 2284 . . 3  |-  A  =  A
21orci 381 . 2  |-  ( A  =  A  \/  A  =  B )
3 elprg 3658 . 2  |-  ( A  e.  V  ->  ( A  e.  { A ,  B }  <->  ( A  =  A  \/  A  =  B ) ) )
42, 3mpbiri 226 1  |-  ( A  e.  V  ->  A  e.  { A ,  B } )
Colors of variables: wff set class
Syntax hints:    -> wi 6    \/ wo 359    = wceq 1628    e. wcel 1688   {cpr 3642
This theorem is referenced by:  prid2g  3734  prid1  3735  opth1  4243  fr2nr  4370  fveqf1o  5767  pw2f1olem  6961  gcdcllem3  12686  pptbas  16739  coseq0negpitopi  19865  vdgr1b  23299  fnckle  25444  kelac2  26562  pmtrprfv  26795
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-sn 3647  df-pr 3648
  Copyright terms: Public domain W3C validator