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

Theorem prid1g 3870
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 2404 . . 3  |-  A  =  A
21orci 380 . 2  |-  ( A  =  A  \/  A  =  B )
3 elprg 3791 . 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 1649    e. wcel 1721   {cpr 3775
This theorem is referenced by:  prid2g  3871  prid1  3872  opth1  4394  fr2nr  4520  fveqf1o  5988  pw2f1olem  7171  gcdcllem3  12968  pptbas  17027  coseq0negpitopi  20364  usgra2edg  21355  nbgraf1olem1  21404  nbgraf1olem3  21406  nbgraf1olem5  21408  nb3graprlem1  21413  nb3graprlem2  21414  constr1trl  21541  vdgr1b  21628  vdusgra0nedg  21632  usgravd0nedg  21636  kelac2  27031  pmtrprfv  27264  imarnf1pr  27965  vdn0frgrav2  28128  vdgn0frgrav2  28129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-sn 3780  df-pr 3781
  Copyright terms: Public domain W3C validator