Theorem elpri 4603

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

Syntax hints:   → wi 4   ∨ wo 858   = wceq 1559   ∈ wcel 2141  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-sn 4580  df-pr 4582

This theorem is referenced by:  elprn1  4607  elprn2  4608  nelpri  4611  nelprd  4613  tppreqb  4762  elpreqpr  4822  elpr2elpr  4824  prproe  4860  3elpr2eq  4861  opth1  5440  0nelop  5462  ftpg  7133  fvf1pr  7285  2oconcl  8465  cantnflem2  9638  eldju1st  9874  m1expcl2  14091  hash2pwpr  14482  bitsinv1lem  16465  prm23lt5  16840  fnpr2ob  17578  fvprif  17581  xpsfeq  17583  ex-chn2  18660  pmtrprfval  19517  m1expaddsub  19528  psgnprfval  19551  frgpuptinv  19801  frgpup3lem  19807  simpgnsgeqd  20133  2nsgsimpgd  20134  simpgnsgbid  20135  cnmsgnsubg  21616  zrhpsgnelbas  21633  mdetralt  22655  m2detleiblem1  22671  indiscld  23138  cnindis  23339  connclo  23462  txindis  23681  xpsxmetlem  24426  xpsmet  24429  ishl2  25419  recnprss  25953  recnperf  25954  dvlip2  26044  coseq0negpitopi  26555  pythag  26869  reasinsin  26948  scvxcvx  27037  perfectlem2  27281  lgslem4  27351  lgseisenlem2  27427  2lgsoddprmlem3  27465  usgredg4  29374  konigsberg  30415  ex-pr  30588  elpreq  32686  1neg1t1neg1  32900  tocyc01  33258  drngidl  33579  drng0mxidl  33624  ply1dg3rt0irred  33740  rtelextdg2  33984  constrconj  34002  signswch  34815  kur14lem7  35522  poimirlem31  38110  ftc1anclem2  38153  wepwsolem  43579  omabs2  43869  omcl3g  43871  relexp01min  44249  clsk1indlem1  44581  mnuprdlem1  44808  mnuprdlem2  44809  mnuprdlem3  44810  mnurndlem1  44817  ssrecnpr  44844  seff  44845  sblpnf  44846  expgrowthi  44869  dvconstbi  44870  sumpair  45575  refsum2cnlem1  45577  iooinlbub  46037  cncfiooicclem1  46427  dvmptconst  46449  dvmptidg  46451  dvmulcncf  46459  dvdivcncf  46461  elprneb  47583  minusmodnep2tmod  47913  perfectALTVlem2  48304  grtriclwlk3  48527  gpgcubic  48661  gpg5nbgr3star  48663  gpgprismgr4cycllem3  48679  gpgprismgr4cycllem7  48683  gpgprismgr4cycllem10  48686  pgnbgreunbgr  48707  0dig2pr01  49192  prelrrx2b  49296  infsubc  49641  infsubc2  49642  setc2othin  50047