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

Theorem elpri 4565
 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 4564 . 2 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
21ibi 269 1 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 843   = wceq 1537   ∈ wcel 2114  {cpr 4545 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475  df-un 3918  df-sn 4544  df-pr 4546 This theorem is referenced by:  nelpri  4570  nelprd  4572  tppreqb  4714  elpreqpr  4773  elpr2elpr  4775  prproe  4812  3elpr2eq  4813  opth1  5343  0nelop  5362  ftpg  6894  2oconcl  8106  cantnflem2  9131  eldju1st  9330  m1expcl2  13436  hash2pwpr  13819  bitsinv1lem  15768  prm23lt5  16129  fnpr2ob  16810  fvprif  16813  xpsfeq  16815  pmtrprfval  18594  m1expaddsub  18605  psgnprfval  18628  frgpuptinv  18876  frgpup3lem  18882  simpgnsgeqd  19202  2nsgsimpgd  19203  simpgnsgbid  19204  cnmsgnsubg  20697  zrhpsgnelbas  20714  mdetralt  21193  m2detleiblem1  21209  indiscld  21675  cnindis  21876  connclo  21999  txindis  22218  xpsxmetlem  22965  xpsmet  22968  ishl2  23953  recnprss  24486  recnperf  24487  dvlip2  24577  coseq0negpitopi  25075  pythag  25382  reasinsin  25461  scvxcvx  25550  perfectlem2  25793  lgslem4  25863  lgseisenlem2  25939  2lgsoddprmlem3  25977  usgredg4  26986  konigsberg  28021  ex-pr  28194  elpreq  30277  1neg1t1neg1  30460  tocyc01  30768  signswch  31839  kur14lem7  32467  poimirlem31  34964  ftc1anclem2  35007  wepwsolem  39779  relexp01min  40193  clsk1indlem1  40530  mnuprdlem1  40763  mnuprdlem2  40764  mnuprdlem3  40765  mnurndlem1  40772  ssrecnpr  40795  seff  40796  sblpnf  40797  expgrowthi  40820  dvconstbi  40821  sumpair  41447  refsum2cnlem1  41449  iooinlbub  41929  elprn1  42066  elprn2  42067  cncfiooicclem1  42326  dvmptconst  42348  dvmptidg  42350  dvmulcncf  42358  dvdivcncf  42360  elprneb  43412  perfectALTVlem2  44032  0dig2pr01  44815  prelrrx2b  44888
 Copyright terms: Public domain W3C validator