Theorem elpri 4390

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

Syntax hints:   → wi 4   ∨ wo 874   = wceq 1653   ∈ wcel 2157  {cpr 4370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-un 3774  df-sn 4369  df-pr 4371

This theorem is referenced by:  nelpri  4393  nelprd  4395  tppreqb  4524  elpreqpr  4587  elpr2elpr  4589  prproe  4626  3elpr2eq  4627  opth1  5134  0nelop  5150  ftpg  6651  2oconcl  7823  cantnflem2  8837  eldju1st  9035  m1expcl2  13136  hash2pwpr  13507  bitsinv1lem  15498  prm23lt5  15852  xpscfv  16537  xpsfeq  16539  pmtrprfval  18219  m1expaddsub  18231  psgnprfval  18254  frgpuptinv  18499  frgpup3lem  18505  cnmsgnsubg  20244  zrhpsgnelbas  20262  mdetralt  20740  m2detleiblem1  20756  indiscld  21224  cnindis  21425  connclo  21547  txindis  21766  xpsxmetlem  22512  xpsmet  22515  ishl2  23496  recnprss  24009  recnperf  24010  dvlip2  24099  coseq0negpitopi  24597  pythag  24899  reasinsin  24975  scvxcvx  25064  perfectlem2  25307  lgslem4  25377  lgseisenlem2  25453  2lgsoddprmlem3  25491  usgredg4  26450  konigsberg  27604  ex-pr  27815  elpreq  29878  1neg1t1neg1  30032  signswch  31156  kur14lem7  31711  poimirlem31  33929  ftc1anclem2  33974  wepwsolem  38397  relexp01min  38788  clsk1indlem1  39125  ssrecnpr  39289  seff  39290  sblpnf  39291  expgrowthi  39314  dvconstbi  39315  sumpair  39954  refsum2cnlem1  39956  iooinlbub  40471  elprn1  40609  elprn2  40610  cncfiooicclem1  40850  dvmptconst  40873  dvmptidg  40875  dvmulcncf  40884  dvdivcncf  40886  elprneb  41917  perfectALTVlem2  42413  0dig2pr01  43203