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

Theorem prid1g 3979
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 2441 . . 3  |-  A  =  A
21orci 390 . 2  |-  ( A  =  A  \/  A  =  B )
3 elprg 3891 . 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 1369    e. wcel 1756   {cpr 3877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-un 3331  df-sn 3876  df-pr 3878
This theorem is referenced by:  prid2g  3980  prid1  3981  opth1  4563  fr2nr  4696  fveqf1o  5998  pw2f1olem  7413  gcdcllem3  13695  pmtrprfv  15957  pptbas  18610  coseq0negpitopi  21963  usgra2edg  23299  nbgraf1olem1  23348  nbgraf1olem3  23350  nbgraf1olem5  23352  nb3graprlem1  23357  nb3graprlem2  23358  constr1trl  23485  vdgr1b  23572  vdusgra0nedg  23576  usgravd0nedg  23580  ftc1anclem8  28471  kelac2  29415  imarnf1pr  30147  vdn0frgrav2  30613  vdgn0frgrav2  30614
  Copyright terms: Public domain W3C validator