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

Theorem prid1g 3934
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 2442 . . 3  |-  A  =  A
21orci 381 . 2  |-  ( A  =  A  \/  A  =  B )
3 elprg 3855 . 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 4    \/ wo 359    = wceq 1653    e. wcel 1727   {cpr 3839
This theorem is referenced by:  prid2g  3935  prid1  3936  opth1  4463  fr2nr  4589  fveqf1o  6058  pw2f1olem  7241  gcdcllem3  13044  pptbas  17103  coseq0negpitopi  20442  usgra2edg  21433  nbgraf1olem1  21482  nbgraf1olem3  21484  nbgraf1olem5  21486  nb3graprlem1  21491  nb3graprlem2  21492  constr1trl  21619  vdgr1b  21706  vdusgra0nedg  21710  usgravd0nedg  21714  ftc1anclem8  26325  kelac2  27178  pmtrprfv  27411  imarnf1pr  28126  vdn0frgrav2  28512  vdgn0frgrav2  28513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-un 3311  df-sn 3844  df-pr 3845
  Copyright terms: Public domain W3C validator