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

Theorem prid1g 3897
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 2430 . . 3  |-  A  =  A
21orci 380 . 2  |-  ( A  =  A  \/  A  =  B )
3 elprg 3818 . 2  |-  ( A  e.  V  ->  ( A  e.  { A ,  B }  <->  ( A  =  A  \/  A  =  B ) ) )
42, 3mpbiri 225 1  |-  ( A  e.  V  ->  A  e.  { A ,  B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    = wceq 1652    e. wcel 1725   {cpr 3802
This theorem is referenced by:  prid2g  3898  prid1  3899  opth1  4421  fr2nr  4547  fveqf1o  6015  pw2f1olem  7198  gcdcllem3  12996  pptbas  17055  coseq0negpitopi  20394  usgra2edg  21385  nbgraf1olem1  21434  nbgraf1olem3  21436  nbgraf1olem5  21438  nb3graprlem1  21443  nb3graprlem2  21444  constr1trl  21571  vdgr1b  21658  vdusgra0nedg  21662  usgravd0nedg  21666  kelac2  27073  pmtrprfv  27306  imarnf1pr  28007  vdn0frgrav2  28170  vdgn0frgrav2  28171
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-v 2945  df-un 3312  df-sn 3807  df-pr 3808
  Copyright terms: Public domain W3C validator