Theorem elpri 4547

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

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1538   ∈ wcel 2111  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  nelpri  4554  nelprd  4556  tppreqb  4698  elpreqpr  4757  elpr2elpr  4759  prproe  4798  3elpr2eq  4799  opth1  5332  0nelop  5351  ftpg  6895  2oconcl  8111  cantnflem2  9137  eldju1st  9336  m1expcl2  13447  hash2pwpr  13830  bitsinv1lem  15780  prm23lt5  16141  fnpr2ob  16823  fvprif  16826  xpsfeq  16828  pmtrprfval  18607  m1expaddsub  18618  psgnprfval  18641  frgpuptinv  18889  frgpup3lem  18895  simpgnsgeqd  19216  2nsgsimpgd  19217  simpgnsgbid  19218  cnmsgnsubg  20266  zrhpsgnelbas  20283  mdetralt  21213  m2detleiblem1  21229  indiscld  21696  cnindis  21897  connclo  22020  txindis  22239  xpsxmetlem  22986  xpsmet  22989  ishl2  23974  recnprss  24507  recnperf  24508  dvlip2  24598  coseq0negpitopi  25096  pythag  25403  reasinsin  25482  scvxcvx  25571  perfectlem2  25814  lgslem4  25884  lgseisenlem2  25960  2lgsoddprmlem3  25998  usgredg4  27007  konigsberg  28042  ex-pr  28215  elpreq  30302  1neg1t1neg1  30499  tocyc01  30810  signswch  31941  kur14lem7  32572  poimirlem31  35088  ftc1anclem2  35131  wepwsolem  39986  relexp01min  40414  clsk1indlem1  40748  mnuprdlem1  40980  mnuprdlem2  40981  mnuprdlem3  40982  mnurndlem1  40989  ssrecnpr  41012  seff  41013  sblpnf  41014  expgrowthi  41037  dvconstbi  41038  sumpair  41664  refsum2cnlem1  41666  iooinlbub  42138  elprn1  42275  elprn2  42276  cncfiooicclem1  42535  dvmptconst  42557  dvmptidg  42559  dvmulcncf  42567  dvdivcncf  42569  elprneb  43621  perfectALTVlem2  44240  0dig2pr01  45024  prelrrx2b  45128