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

Theorem prid1g 4121
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 2443 . . 3  |-  A  =  A
21orci 390 . 2  |-  ( A  =  A  \/  A  =  B )
3 elprg 4030 . 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 1383    e. wcel 1804   {cpr 4016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-sn 4015  df-pr 4017
This theorem is referenced by:  prid2g  4122  prid1  4123  opth1  4710  fr2nr  4847  fveqf1o  6190  pw2f1olem  7623  hashprdifel  12445  gcdcllem3  14133  mgm2nsgrplem1  16015  mgm2nsgrplem2  16016  mgm2nsgrplem3  16017  sgrp2nmndlem1  16020  sgrp2rid2  16023  pmtrprfv  16457  pptbas  19487  coseq0negpitopi  22874  usgra2edg  24360  nbgraf1olem1  24419  nbgraf1olem3  24421  nbgraf1olem5  24423  nb3graprlem1  24429  nb3graprlem2  24430  constr1trl  24568  vdgr1b  24882  vdusgra0nedg  24886  usgravd0nedg  24896  vdn0frgrav2  25001  vdgn0frgrav2  25002  ftc1anclem8  30073  kelac2  30987  fourierdlem54  31897  imarnf1pr  32263  usgvad2edg  32365
  Copyright terms: Public domain W3C validator