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

Theorem prid1g 3541
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 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})

Proof of Theorem prid1g
StepHypRef Expression
1 eqid 2088 . . 3 𝐴 = 𝐴
21orci 685 . 2 (𝐴 = 𝐴𝐴 = 𝐵)
3 elprg 3461 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴𝐴 = 𝐵)))
42, 3mpbiri 166 1 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
Colors of variables: wff set class
Syntax hints:  wi 4  wo 664   = wceq 1289  wcel 1438  {cpr 3442
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-sn 3447  df-pr 3448
This theorem is referenced by:  prid2g  3542  prid1  3543  preqr1g  3605  opth1  4054  en2lp  4360  acexmidlemcase  5629  en2eqpr  6603  m1expcl2  9942  maxabslemval  10606
  Copyright terms: Public domain W3C validator