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

Theorem elpr 3582
Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)
Hypothesis
Ref Expression
elpr.1 𝐴 ∈ V
Assertion
Ref Expression
elpr (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶))

Proof of Theorem elpr
StepHypRef Expression
1 elpr.1 . 2 𝐴 ∈ V
2 elprg 3581 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶))
Colors of variables: wff set class
Syntax hints:  wb 104  wo 698   = wceq 1335  wcel 2128  Vcvv 2712  {cpr 3562
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 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3567  df-pr 3568
This theorem is referenced by:  prmg  3682  difprsnss  3696  preqr1  3733  preq12b  3735  prel12  3736  pwprss  3770  pwtpss  3771  unipr  3788  intpr  3841  zfpair2  4172  elop  4193  ordtri2or2exmidlem  4487  onsucelsucexmidlem  4490  en2lp  4515  reg3exmidlemwe  4540  xpsspw  4700  acexmidlem2  5823  2oconcl  6388  exmidpw  6855  exmidpweq  6856  renfdisj  7939  fzpr  9985  maxabslemval  11119  xrmaxiflemval  11158  isprm2  12009  bj-zfpair2  13556  ss1oel2o  13636
  Copyright terms: Public domain W3C validator