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

Theorem prid1g 4080
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 390 . 2  |-  ( A  =  A  \/  A  =  B )
3 elprg 3990 . 2  |-  ( A  e.  V  ->  ( A  e.  { A ,  B }  <->  ( A  =  A  \/  A  =  B ) ) )
42, 3mpbiri 235 1  |-  ( A  e.  V  ->  A  e.  { A ,  B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    = wceq 1407    e. wcel 1844   {cpr 3976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-v 3063  df-un 3421  df-sn 3975  df-pr 3977
This theorem is referenced by:  prid2g  4081  prid1  4082  opth1  4666  fr2nr  4803  fpr2g  6114  f1prex  6172  fveqf1o  6190  pw2f1olem  7661  hashprdifel  12514  gcdcllem3  14362  mgm2nsgrplem1  16362  mgm2nsgrplem2  16363  mgm2nsgrplem3  16364  sgrp2nmndlem1  16367  sgrp2rid2  16370  pmtrprfv  16804  pptbas  19803  coseq0negpitopi  23190  usgra2edg  24811  nbgraf1olem1  24870  nbgraf1olem3  24872  nbgraf1olem5  24874  nb3graprlem1  24880  nb3graprlem2  24881  constr1trl  25019  vdgr1b  25333  vdusgra0nedg  25337  usgravd0nedg  25347  vdn0frgrav2  25452  vdgn0frgrav2  25453  ftc1anclem8  31483  kelac2  35386  fourierdlem54  37324  imarnf1pr  37955  usgvad2edg  38053
  Copyright terms: Public domain W3C validator