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

Theorem prid1g 3732
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 2283 . . 3  |-  A  =  A
21orci 379 . 2  |-  ( A  =  A  \/  A  =  B )
3 elprg 3657 . 2  |-  ( A  e.  V  ->  ( A  e.  { A ,  B }  <->  ( A  =  A  \/  A  =  B ) ) )
42, 3mpbiri 224 1  |-  ( A  e.  V  ->  A  e.  { A ,  B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    = wceq 1623    e. wcel 1684   {cpr 3641
This theorem is referenced by:  prid2g  3733  prid1  3734  opth1  4244  fr2nr  4371  fveqf1o  5806  pw2f1olem  6966  gcdcllem3  12692  pptbas  16745  coseq0negpitopi  19871  vdgr1b  23895  fnckle  26045  kelac2  27163  pmtrprfv  27396
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator