Theorem elpri 4604

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 4603	. 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
2	1	ibi 267	1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  elprn1  4608  elprn2  4609  nelpri  4612  nelprd  4614  tppreqb  4761  elpreqpr  4823  elpr2elpr  4825  prproe  4861  3elpr2eq  4862  opth1  5423  0nelop  5444  ftpg  7101  fvf1pr  7253  2oconcl  8430  cantnflem2  9599  eldju1st  9835  m1expcl2  14008  hash2pwpr  14399  bitsinv1lem  16368  prm23lt5  16742  fnpr2ob  17479  fvprif  17482  xpsfeq  17484  ex-chn2  18561  pmtrprfval  19416  m1expaddsub  19427  psgnprfval  19450  frgpuptinv  19700  frgpup3lem  19706  simpgnsgeqd  20032  2nsgsimpgd  20033  simpgnsgbid  20034  cnmsgnsubg  21532  zrhpsgnelbas  21549  mdetralt  22552  m2detleiblem1  22568  indiscld  23035  cnindis  23236  connclo  23359  txindis  23578  xpsxmetlem  24323  xpsmet  24326  ishl2  25326  recnprss  25861  recnperf  25862  dvlip2  25956  coseq0negpitopi  26468  pythag  26783  reasinsin  26862  scvxcvx  26952  perfectlem2  27197  lgslem4  27267  lgseisenlem2  27343  2lgsoddprmlem3  27381  usgredg4  29290  konigsberg  30332  ex-pr  30505  elpreq  32603  1neg1t1neg1  32817  tocyc01  33200  drngidl  33514  drng0mxidl  33557  ply1dg3rt0irred  33665  rtelextdg2  33884  constrconj  33902  signswch  34718  kur14lem7  35406  poimirlem31  37852  ftc1anclem2  37895  wepwsolem  43284  omabs2  43574  omcl3g  43576  relexp01min  43954  clsk1indlem1  44286  mnuprdlem1  44513  mnuprdlem2  44514  mnuprdlem3  44515  mnurndlem1  44522  ssrecnpr  44549  seff  44550  sblpnf  44551  expgrowthi  44574  dvconstbi  44575  sumpair  45280  refsum2cnlem1  45282  iooinlbub  45747  cncfiooicclem1  46137  dvmptconst  46159  dvmptidg  46161  dvmulcncf  46169  dvdivcncf  46171  elprneb  47275  minusmodnep2tmod  47599  perfectALTVlem2  47968  grtriclwlk3  48191  gpgcubic  48325  gpg5nbgr3star  48327  gpgprismgr4cycllem3  48343  gpgprismgr4cycllem7  48347  gpgprismgr4cycllem10  48350  pgnbgreunbgr  48371  0dig2pr01  48856  prelrrx2b  48960  infsubc  49305  infsubc2  49306  setc2othin  49711