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

Theorem prid1 3543
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 𝐴 ∈ V
Assertion
Ref Expression
prid1 𝐴 ∈ {𝐴, 𝐵}

Proof of Theorem prid1
StepHypRef Expression
1 prid1.1 . 2 𝐴 ∈ V
2 prid1g 3541 . 2 (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
31, 2ax-mp 7 1 𝐴 ∈ {𝐴, 𝐵}
Colors of variables: wff set class
Syntax hints:  wcel 1438  Vcvv 2619  {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:  prid2  3544  prnz  3557  preqr1  3607  preq12b  3609  prel12  3610  opi1  4050  opeluu  4263  onsucelsucexmidlem1  4334  regexmidlem1  4339  reg2exmidlema  4340  opthreg  4362  ordtri2or2exmid  4377  dmrnssfld  4684  funopg  5034  acexmidlemb  5626  2dom  6502  unfiexmid  6608  djuss  6740  exmidomni  6777  fodjuomnilemf  6779  reelprrecn  7456  pnfxr  7519  bdop  11412  0lt2o  11531
  Copyright terms: Public domain W3C validator