Theorem elpri 4613

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  nelpri  4619  nelprd  4621  tppreqb  4769  elpreqpr  4831  elpr2elpr  4833  prproe  4869  3elpr2eq  4870  opth1  5435  0nelop  5456  ftpg  7128  fvf1pr  7282  2oconcl  8467  cantnflem2  9643  eldju1st  9876  m1expcl2  14050  hash2pwpr  14441  bitsinv1lem  16411  prm23lt5  16785  fnpr2ob  17521  fvprif  17524  xpsfeq  17526  pmtrprfval  19417  m1expaddsub  19428  psgnprfval  19451  frgpuptinv  19701  frgpup3lem  19707  simpgnsgeqd  20033  2nsgsimpgd  20034  simpgnsgbid  20035  cnmsgnsubg  21486  zrhpsgnelbas  21503  mdetralt  22495  m2detleiblem1  22511  indiscld  22978  cnindis  23179  connclo  23302  txindis  23521  xpsxmetlem  24267  xpsmet  24270  ishl2  25270  recnprss  25805  recnperf  25806  dvlip2  25900  coseq0negpitopi  26412  pythag  26727  reasinsin  26806  scvxcvx  26896  perfectlem2  27141  lgslem4  27211  lgseisenlem2  27287  2lgsoddprmlem3  27325  usgredg4  29144  konigsberg  30186  ex-pr  30359  elpreq  32457  1neg1t1neg1  32661  tocyc01  33075  drngidl  33404  drng0mxidl  33447  ply1dg3rt0irred  33551  rtelextdg2  33717  constrconj  33735  signswch  34552  kur14lem7  35199  poimirlem31  37645  ftc1anclem2  37688  wepwsolem  43031  omabs2  43321  omcl3g  43323  relexp01min  43702  clsk1indlem1  44034  mnuprdlem1  44261  mnuprdlem2  44262  mnuprdlem3  44263  mnurndlem1  44270  ssrecnpr  44297  seff  44298  sblpnf  44299  expgrowthi  44322  dvconstbi  44323  sumpair  45029  refsum2cnlem1  45031  iooinlbub  45499  elprn1  45631  elprn2  45632  cncfiooicclem1  45891  dvmptconst  45913  dvmptidg  45915  dvmulcncf  45923  dvdivcncf  45925  elprneb  47030  minusmodnep2tmod  47354  perfectALTVlem2  47723  grtriclwlk3  47944  gpgcubic  48070  gpg5nbgr3star  48072  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem10  48094  pgnbgreunbgr  48115  0dig2pr01  48599  prelrrx2b  48703  infsubc  49049  infsubc2  49050  setc2othin  49455