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

Theorem prid1 3531
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 3529 . 2  |-  ( A  e.  _V  ->  A  e.  { A ,  B } )
31, 2ax-mp 7 1  |-  A  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1436   _Vcvv 2615   {cpr 3432
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438
This theorem is referenced by:  prid2  3532  prnz  3545  preqr1  3595  preq12b  3597  prel12  3598  opi1  4033  opeluu  4246  onsucelsucexmidlem1  4317  regexmidlem1  4322  reg2exmidlema  4323  opthreg  4345  ordtri2or2exmid  4360  dmrnssfld  4664  funopg  5013  acexmidlemb  5605  2dom  6474  unfiexmid  6580  djuss  6705  exmidomni  6742  fodjuomnilemf  6744  reelprrecn  7421  pnfxr  7484  bdop  11211  0lt2o  11330
  Copyright terms: Public domain W3C validator