Theorem elpri 4601

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

Step	Hyp	Ref	Expression
1		elprg 4600	. 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
2	1	ibi 267	1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2113  {cpr 4579

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-pr 4580

This theorem is referenced by:  elprn1  4605  elprn2  4606  nelpri  4609  nelprd  4611  tppreqb  4758  elpreqpr  4820  elpr2elpr  4822  prproe  4858  3elpr2eq  4859  opth1  5420  0nelop  5441  ftpg  7097  fvf1pr  7249  2oconcl  8426  cantnflem2  9589  eldju1st  9825  m1expcl2  13996  hash2pwpr  14387  bitsinv1lem  16356  prm23lt5  16730  fnpr2ob  17466  fvprif  17469  xpsfeq  17471  ex-chn2  18548  pmtrprfval  19403  m1expaddsub  19414  psgnprfval  19437  frgpuptinv  19687  frgpup3lem  19693  simpgnsgeqd  20019  2nsgsimpgd  20020  simpgnsgbid  20021  cnmsgnsubg  21518  zrhpsgnelbas  21535  mdetralt  22526  m2detleiblem1  22542  indiscld  23009  cnindis  23210  connclo  23333  txindis  23552  xpsxmetlem  24297  xpsmet  24300  ishl2  25300  recnprss  25835  recnperf  25836  dvlip2  25930  coseq0negpitopi  26442  pythag  26757  reasinsin  26836  scvxcvx  26926  perfectlem2  27171  lgslem4  27241  lgseisenlem2  27317  2lgsoddprmlem3  27355  usgredg4  29199  konigsberg  30241  ex-pr  30414  elpreq  32512  1neg1t1neg1  32727  tocyc01  33096  drngidl  33407  drng0mxidl  33450  ply1dg3rt0irred  33555  rtelextdg2  33763  constrconj  33781  signswch  34597  kur14lem7  35279  poimirlem31  37714  ftc1anclem2  37757  wepwsolem  43162  omabs2  43452  omcl3g  43454  relexp01min  43833  clsk1indlem1  44165  mnuprdlem1  44392  mnuprdlem2  44393  mnuprdlem3  44394  mnurndlem1  44401  ssrecnpr  44428  seff  44429  sblpnf  44430  expgrowthi  44453  dvconstbi  44454  sumpair  45159  refsum2cnlem1  45161  iooinlbub  45628  cncfiooicclem1  46018  dvmptconst  46040  dvmptidg  46042  dvmulcncf  46050  dvdivcncf  46052  elprneb  47156  minusmodnep2tmod  47480  perfectALTVlem2  47849  grtriclwlk3  48072  gpgcubic  48206  gpg5nbgr3star  48208  gpgprismgr4cycllem3  48224  gpgprismgr4cycllem7  48228  gpgprismgr4cycllem10  48231  pgnbgreunbgr  48252  0dig2pr01  48738  prelrrx2b  48842  infsubc  49188  infsubc2  49189  setc2othin  49594