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

Theorem prid1 3597
 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 3595 . 2 (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
31, 2ax-mp 5 1 𝐴 ∈ {𝐴, 𝐵}
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1463  Vcvv 2658  {cpr 3496 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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502 This theorem is referenced by:  prid2  3598  prnz  3613  preqr1  3663  preq12b  3665  prel12  3666  opi1  4122  opeluu  4339  onsucelsucexmidlem1  4411  regexmidlem1  4416  reg2exmidlema  4417  opthreg  4439  ordtri2or2exmid  4454  dmrnssfld  4770  funopg  5125  acexmidlemb  5732  0lt2o  6304  2dom  6665  unfiexmid  6772  djuss  6921  exmidomni  6980  exmidaclem  7028  reelprrecn  7719  pnfxr  7782  sup3exmid  8675  bdop  12907  isomninnlem  13059
 Copyright terms: Public domain W3C validator