Theorem elpri 4419

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

Syntax hints:   → wi 4   ∨ wo 878   = wceq 1656   ∈ wcel 2164  {cpr 4399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-un 3803  df-sn 4398  df-pr 4400

This theorem is referenced by:  nelpri  4422  nelprd  4424  tppreqb  4554  elpreqpr  4617  elpr2elpr  4619  prproe  4656  3elpr2eq  4657  opth1  5164  0nelop  5180  ftpg  6674  2oconcl  7850  cantnflem2  8864  eldju1st  9062  m1expcl2  13176  hash2pwpr  13547  bitsinv1lem  15536  prm23lt5  15890  xpscfv  16575  xpsfeq  16577  pmtrprfval  18257  m1expaddsub  18269  psgnprfval  18292  frgpuptinv  18537  frgpup3lem  18543  cnmsgnsubg  20282  zrhpsgnelbas  20300  mdetralt  20782  m2detleiblem1  20798  indiscld  21266  cnindis  21467  connclo  21589  txindis  21808  xpsxmetlem  22554  xpsmet  22557  ishl2  23538  recnprss  24067  recnperf  24068  dvlip2  24157  coseq0negpitopi  24655  pythag  24957  reasinsin  25036  scvxcvx  25125  perfectlem2  25368  lgslem4  25438  lgseisenlem2  25514  2lgsoddprmlem3  25552  usgredg4  26513  konigsberg  27625  ex-pr  27834  elpreq  29897  1neg1t1neg1  30050  signswch  31174  kur14lem7  31729  poimirlem31  33977  ftc1anclem2  34022  wepwsolem  38448  relexp01min  38839  clsk1indlem1  39176  ssrecnpr  39340  seff  39341  sblpnf  39342  expgrowthi  39365  dvconstbi  39366  sumpair  40005  refsum2cnlem1  40007  iooinlbub  40515  elprn1  40653  elprn2  40654  cncfiooicclem1  40894  dvmptconst  40917  dvmptidg  40919  dvmulcncf  40928  dvdivcncf  40930  elprneb  41958  perfectALTVlem2  42454  0dig2pr01  43244