Theorem elpri 4609

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

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1563   ∈ wcel 2145  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588

This theorem is referenced by:  elprn1  4613  elprn2  4614  nelpri  4617  nelprd  4619  tppreqb  4768  elpreqpr  4827  elpr2elpr  4829  prproe  4865  3elpr2eq  4866  opth1  5447  0nelop  5469  ftpg  7143  fvf1pr  7295  2oconcl  8476  cantnflem2  9647  eldju1st  9897  m1expcl2  14109  hash2pwpr  14501  bitsinv1lem  16487  prm23lt5  16862  fnpr2ob  17600  fvprif  17603  xpsfeq  17605  ex-chn2  18682  pmtrprfval  19545  m1expaddsub  19556  psgnprfval  19579  frgpuptinv  19829  frgpup3lem  19835  simpgnsgeqd  20161  2nsgsimpgd  20162  simpgnsgbid  20163  cnmsgnsubg  21684  zrhpsgnelbas  21701  mdetralt  22722  m2detleiblem1  22738  indiscld  23205  cnindis  23406  connclo  23529  txindis  23748  xpsxmetlem  24493  xpsmet  24496  ishl2  25486  recnprss  26020  recnperf  26021  dvlip2  26111  coseq0negpitopi  26622  pythag  26936  reasinsin  27015  scvxcvx  27104  perfectlem2  27348  lgslem4  27418  lgseisenlem2  27494  2lgsoddprmlem3  27532  usgredg4  29472  konigsberg  30513  ex-pr  30686  elpreq  32780  1neg1t1neg1  32991  tocyc01  33346  drngidl  33652  drng0mxidl  33670  ply1dg3rt0irred  33786  rtelextdg2  34029  constrconj  34047  signswch  34860  kur14lem7  35570  poimirlem31  38157  ftc1anclem2  38200  wepwsolem  43626  omabs2  43916  omcl3g  43918  relexp01min  44296  clsk1indlem1  44628  mnuprdlem1  44841  mnuprdlem2  44842  mnuprdlem3  44843  mnurndlem1  44850  ssrecnpr  44877  seff  44878  sblpnf  44879  expgrowthi  44902  dvconstbi  44903  sumpair  45614  refsum2cnlem1  45616  iooinlbub  46076  cncfiooicclem1  46466  dvmptconst  46488  dvmptidg  46490  dvmulcncf  46498  dvdivcncf  46500  elprneb  47622  minusmodnep2tmod  47952  perfectALTVlem2  48343  grtriclwlk3  48566  gpgcubic  48700  gpg5nbgr3star  48702  gpgprismgr4cycllem3  48718  gpgprismgr4cycllem7  48722  gpgprismgr4cycllem10  48725  pgnbgreunbgr  48746  0dig2pr01  49242  prelrrx2b  49346  infsubc  49690  infsubc2  49691  setc2othin  50096