Theorem elpri 4230

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

Syntax hints:   → wi 4   ∨ wo 382   = wceq 1523   ∈ wcel 2030  {cpr 4212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-sn 4211  df-pr 4213

This theorem is referenced by:  elpr2OLD  4233  nelpri  4234  nelprd  4236  tppreqb  4368  elpreqpr  4427  elpr2elpr  4429  prproe  4466  3elpr2eq  4467  opth1  4973  0nelop  4989  funtpgOLD  5981  ftpg  6463  2oconcl  7628  cantnflem2  8625  m1expcl2  12922  hash2pwpr  13296  bitsinv1lem  15210  prm23lt5  15566  xpscfv  16269  xpsfeq  16271  pmtrprfval  17953  m1expaddsub  17964  psgnprfval  17987  frgpuptinv  18230  frgpup3lem  18236  cnmsgnsubg  19971  zrhpsgnelbas  19988  mdetralt  20462  m2detleiblem1  20478  indiscld  20943  cnindis  21144  connclo  21266  txindis  21485  xpsxmetlem  22231  xpsmet  22234  ishl2  23212  recnprss  23713  recnperf  23714  dvlip2  23803  coseq0negpitopi  24300  pythag  24592  reasinsin  24668  scvxcvx  24757  perfectlem2  25000  lgslem4  25070  lgseisenlem2  25146  2lgsoddprmlem3  25184  usgredg4  26154  konigsberg  27235  ex-pr  27417  elpreq  29486  1neg1t1neg1  29642  signswch  30766  kur14lem7  31320  poimirlem31  33570  ftc1anclem2  33616  wepwsolem  37929  relexp01min  38322  clsk1indlem1  38660  ssrecnpr  38824  seff  38825  sblpnf  38826  expgrowthi  38849  dvconstbi  38850  sumpair  39508  refsum2cnlem1  39510  iooinlbub  40041  elprn1  40183  elprn2  40184  cncfiooicclem1  40424  dvmptconst  40447  dvmptidg  40449  dvmulcncf  40458  dvdivcncf  40460  elprneb  41620  perfectALTVlem2  41956  0dig2pr01  42729