ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  prid1 Unicode version

Theorem prid1 3629
Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
prid1.1  |-  A  e. 
_V
Assertion
Ref Expression
prid1  |-  A  e. 
{ A ,  B }

Proof of Theorem prid1
StepHypRef Expression
1 prid1.1 . 2  |-  A  e. 
_V
2 prid1g 3627 . 2  |-  ( A  e.  _V  ->  A  e.  { A ,  B } )
31, 2ax-mp 5 1  |-  A  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1480   _Vcvv 2686   {cpr 3528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534
This theorem is referenced by:  prid2  3630  prnz  3645  preqr1  3695  preq12b  3697  prel12  3698  opi1  4154  opeluu  4371  onsucelsucexmidlem1  4443  regexmidlem1  4448  reg2exmidlema  4449  opthreg  4471  ordtri2or2exmid  4486  dmrnssfld  4802  funopg  5157  acexmidlemb  5766  0lt2o  6338  2dom  6699  unfiexmid  6806  djuss  6955  exmidomni  7014  exmidonfinlem  7054  exmidaclem  7069  reelprrecn  7767  pnfxr  7830  sup3exmid  8727  bdop  13132  isomninnlem  13286
  Copyright terms: Public domain W3C validator