Theorem elpri 4653

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1536   ∈ wcel 2105  {cpr 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-sn 4631  df-pr 4633

This theorem is referenced by:  nelpri  4659  nelprd  4661  tppreqb  4809  elpreqpr  4871  elpr2elpr  4873  prproe  4909  3elpr2eq  4910  opth1  5485  0nelop  5505  ftpg  7175  fvf1pr  7326  2oconcl  8539  cantnflem2  9727  eldju1st  9960  m1expcl2  14122  hash2pwpr  14511  bitsinv1lem  16474  prm23lt5  16847  fnpr2ob  17604  fvprif  17607  xpsfeq  17609  pmtrprfval  19519  m1expaddsub  19530  psgnprfval  19553  frgpuptinv  19803  frgpup3lem  19809  simpgnsgeqd  20135  2nsgsimpgd  20136  simpgnsgbid  20137  cnmsgnsubg  21612  zrhpsgnelbas  21629  mdetralt  22629  m2detleiblem1  22645  indiscld  23114  cnindis  23315  connclo  23438  txindis  23657  xpsxmetlem  24404  xpsmet  24407  ishl2  25417  recnprss  25953  recnperf  25954  dvlip2  26048  coseq0negpitopi  26559  pythag  26874  reasinsin  26953  scvxcvx  27043  perfectlem2  27288  lgslem4  27358  lgseisenlem2  27434  2lgsoddprmlem3  27472  usgredg4  29248  konigsberg  30285  ex-pr  30458  elpreq  32555  1neg1t1neg1  32754  tocyc01  33120  drngidl  33440  drng0mxidl  33483  ply1dg3rt0irred  33586  rtelextdg2  33732  constrconj  33749  signswch  34554  kur14lem7  35196  poimirlem31  37637  ftc1anclem2  37680  wepwsolem  43030  omabs2  43321  omcl3g  43323  relexp01min  43702  clsk1indlem1  44034  mnuprdlem1  44267  mnuprdlem2  44268  mnuprdlem3  44269  mnurndlem1  44276  ssrecnpr  44303  seff  44304  sblpnf  44305  expgrowthi  44328  dvconstbi  44329  sumpair  44972  refsum2cnlem1  44974  iooinlbub  45453  elprn1  45588  elprn2  45589  cncfiooicclem1  45848  dvmptconst  45870  dvmptidg  45872  dvmulcncf  45880  dvdivcncf  45882  elprneb  46978  minusmodnep2tmod  47292  perfectALTVlem2  47646  grtriclwlk3  47849  gpgcubic  47969  gpg5nbgr3star  47971  0dig2pr01  48459  prelrrx2b  48563  setc2othin  48856