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

Theorem elpri 4145
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 4144 . 2 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
21ibi 255 1 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382   = wceq 1475  wcel 1977  {cpr 4127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128
This theorem is referenced by:  elpr2OLD  4148  nelpri  4149  nelprd  4151  tppreqb  4277  elpreqpr  4334  elpr2elpr  4336  opth1  4870  0nelop  4886  funtpgOLD  5857  ftpg  6328  2oconcl  7470  cantnflem2  8470  m1expcl2  12744  hash2pwpr  13115  bitsinv1lem  15001  prm23lt5  15357  xpscfv  16045  xpsfeq  16047  pmtrprfval  17730  m1expaddsub  17741  psgnprfval  17764  frgpuptinv  18007  frgpup3lem  18013  cnmsgnsubg  19742  zrhpsgnelbas  19759  mdetralt  20233  m2detleiblem1  20249  indiscld  20705  cnindis  20906  conclo  21028  txindis  21247  xpsxmetlem  21994  xpsmet  21997  ishl2  22974  recnprss  23474  recnperf  23475  dvlip2  23562  coseq0negpitopi  24059  pythag  24347  reasinsin  24423  scvxcvx  24512  perfectlem2  24755  lgslem4  24825  lgseisenlem2  24901  2lgsoddprmlem3  24939  usgraedg4  25916  cusgrares  26001  2pthlem2  26126  vdgr1a  26433  konigsberg  26514  ex-pr  26679  elpreq  28744  1neg1t1neg1  28902  signswch  29964  kur14lem7  30448  poimirlem31  32610  ftc1anclem2  32656  wepwsolem  36630  relexp01min  37024  clsk1indlem1  37363  ssrecnpr  37529  seff  37530  sblpnf  37531  expgrowthi  37554  dvconstbi  37555  sumpair  38217  refsum2cnlem1  38219  iooinlbub  38570  elprn1  38700  elprn2  38701  cncfiooicclem1  38779  dvmptconst  38803  dvmptidg  38805  dvmulcncf  38815  dvdivcncf  38817  elprneb  39939  perfectALTVlem2  40165  usgredg4  40444  konigsberg-av  41427  0dig2pr01  42202
  Copyright terms: Public domain W3C validator