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

Theorem elpri 4580
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 4579 . 2 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
21ibi 270 1 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847   = wceq 1543  wcel 2112  {cpr 4560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-v 3425  df-un 3888  df-sn 4559  df-pr 4561
This theorem is referenced by:  nelpri  4587  nelprd  4589  tppreqb  4735  elpreqpr  4794  elpr2elpr  4796  prproe  4834  3elpr2eq  4835  opth1  5376  0nelop  5396  ftpg  6993  2oconcl  8254  cantnflem2  9335  eldju1st  9569  m1expcl2  13689  hash2pwpr  14075  bitsinv1lem  16033  prm23lt5  16400  fnpr2ob  17096  fvprif  17099  xpsfeq  17101  pmtrprfval  18912  m1expaddsub  18923  psgnprfval  18946  frgpuptinv  19194  frgpup3lem  19200  simpgnsgeqd  19521  2nsgsimpgd  19522  simpgnsgbid  19523  cnmsgnsubg  20572  zrhpsgnelbas  20589  mdetralt  21537  m2detleiblem1  21553  indiscld  22020  cnindis  22221  connclo  22344  txindis  22563  xpsxmetlem  23309  xpsmet  23312  ishl2  24299  recnprss  24833  recnperf  24834  dvlip2  24924  coseq0negpitopi  25425  pythag  25732  reasinsin  25811  scvxcvx  25900  perfectlem2  26143  lgslem4  26213  lgseisenlem2  26289  2lgsoddprmlem3  26327  usgredg4  27337  konigsberg  28372  ex-pr  28545  elpreq  30629  1neg1t1neg1  30824  tocyc01  31136  signswch  32284  kur14lem7  32918  poimirlem31  35582  ftc1anclem2  35625  wepwsolem  40618  relexp01min  41046  clsk1indlem1  41380  mnuprdlem1  41611  mnuprdlem2  41612  mnuprdlem3  41613  mnurndlem1  41620  ssrecnpr  41647  seff  41648  sblpnf  41649  expgrowthi  41672  dvconstbi  41673  sumpair  42299  refsum2cnlem1  42301  iooinlbub  42760  elprn1  42895  elprn2  42896  cncfiooicclem1  43155  dvmptconst  43177  dvmptidg  43179  dvmulcncf  43187  dvdivcncf  43189  elprneb  44241  perfectALTVlem2  44893  0dig2pr01  45675  prelrrx2b  45779  setc2othin  46056
  Copyright terms: Public domain W3C validator