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

Theorem elpri 4613
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 4612 . 2 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
21ibi 267 1 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846   = wceq 1542  wcel 2107  {cpr 4593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920  df-sn 4592  df-pr 4594
This theorem is referenced by:  nelpri  4620  nelprd  4622  tppreqb  4770  elpreqpr  4829  elpr2elpr  4831  prproe  4868  3elpr2eq  4869  opth1  5437  0nelop  5458  ftpg  7107  2oconcl  8454  cantnflem2  9633  eldju1st  9866  m1expcl2  13998  hash2pwpr  14382  bitsinv1lem  16328  prm23lt5  16693  fnpr2ob  17447  fvprif  17450  xpsfeq  17452  pmtrprfval  19276  m1expaddsub  19287  psgnprfval  19310  frgpuptinv  19560  frgpup3lem  19566  simpgnsgeqd  19887  2nsgsimpgd  19888  simpgnsgbid  19889  cnmsgnsubg  20997  zrhpsgnelbas  21014  mdetralt  21973  m2detleiblem1  21989  indiscld  22458  cnindis  22659  connclo  22782  txindis  23001  xpsxmetlem  23748  xpsmet  23751  ishl2  24750  recnprss  25284  recnperf  25285  dvlip2  25375  coseq0negpitopi  25876  pythag  26183  reasinsin  26262  scvxcvx  26351  perfectlem2  26594  lgslem4  26664  lgseisenlem2  26740  2lgsoddprmlem3  26778  usgredg4  28207  konigsberg  29243  ex-pr  29416  elpreq  31499  1neg1t1neg1  31696  tocyc01  32009  signswch  33213  kur14lem7  33846  poimirlem31  36138  ftc1anclem2  36181  wepwsolem  41398  omabs2  41696  omcl3g  41698  relexp01min  42059  clsk1indlem1  42391  mnuprdlem1  42626  mnuprdlem2  42627  mnuprdlem3  42628  mnurndlem1  42635  ssrecnpr  42662  seff  42663  sblpnf  42664  expgrowthi  42687  dvconstbi  42688  sumpair  43314  refsum2cnlem1  43316  iooinlbub  43813  elprn1  43948  elprn2  43949  cncfiooicclem1  44208  dvmptconst  44230  dvmptidg  44232  dvmulcncf  44240  dvdivcncf  44242  elprneb  45337  perfectALTVlem2  45988  0dig2pr01  46770  prelrrx2b  46874  setc2othin  47150
  Copyright terms: Public domain W3C validator