MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpri Structured version   Visualization version   GIF version

Theorem elpri 4140
Description: If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.)
Assertion
Ref Expression
elpri (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))

Proof of Theorem elpri
StepHypRef Expression
1 elprg 4139 . 2 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
21ibi 254 1 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381   = wceq 1474  wcel 1975  {cpr 4122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-un 3540  df-sn 4121  df-pr 4123
This theorem is referenced by:  elpr2OLD  4143  nelpri  4144  nelprd  4146  tppreqb  4272  elpreqpr  4325  opth1  4860  0nelop  4876  funtpgOLD  5839  ftpg  6302  2oconcl  7443  cantnflem2  8443  m1expcl2  12695  hash2pwpr  13061  bitsinv1lem  14943  prm23lt5  15299  xpscfv  15987  xpsfeq  15989  pmtrprfval  17672  m1expaddsub  17683  psgnprfval  17706  frgpuptinv  17949  frgpup3lem  17955  cnmsgnsubg  19683  zrhpsgnelbas  19700  mdetralt  20171  m2detleiblem1  20187  indiscld  20643  cnindis  20844  conclo  20966  txindis  21185  xpsxmetlem  21931  xpsmet  21934  ishl2  22887  recnprss  23387  recnperf  23388  dvlip2  23475  coseq0negpitopi  23972  pythag  24260  reasinsin  24336  scvxcvx  24425  perfectlem2  24668  lgslem4  24738  lgseisenlem2  24814  2lgsoddprmlem3  24852  usgraedg4  25678  cusgrares  25763  2pthlem2  25888  vdgr1a  26195  konigsberg  26276  ex-pr  26441  elpreq  28546  1neg1t1neg1  28704  signswch  29766  kur14lem7  30250  poimirlem31  32409  ftc1anclem2  32455  wepwsolem  36429  relexp01min  36823  clsk1indlem1  37162  ssrecnpr  37328  seff  37329  sblpnf  37330  expgrowthi  37353  dvconstbi  37354  sumpair  38016  refsum2cnlem1  38018  iooinlbub  38370  elprn1  38500  elprn2  38501  cncfiooicclem1  38579  dvmptconst  38603  dvmptidg  38605  dvmulcncf  38615  dvdivcncf  38617  elprneb  39740  perfectALTVlem2  39966  elpr2elpr  40126  usgredg4  40442  konigsberg-av  41425  0dig2pr01  42200
  Copyright terms: Public domain W3C validator