Theorem elpri 4592

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114  {cpr 4570

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  elprn1  4596  elprn2  4597  nelpri  4600  nelprd  4602  tppreqb  4749  elpreqpr  4811  elpr2elpr  4813  prproe  4849  3elpr2eq  4850  opth1  5423  0nelop  5444  ftpg  7103  fvf1pr  7255  2oconcl  8431  cantnflem2  9602  eldju1st  9838  m1expcl2  14038  hash2pwpr  14429  bitsinv1lem  16401  prm23lt5  16776  fnpr2ob  17513  fvprif  17516  xpsfeq  17518  ex-chn2  18595  pmtrprfval  19453  m1expaddsub  19464  psgnprfval  19487  frgpuptinv  19737  frgpup3lem  19743  simpgnsgeqd  20069  2nsgsimpgd  20070  simpgnsgbid  20071  cnmsgnsubg  21567  zrhpsgnelbas  21584  mdetralt  22583  m2detleiblem1  22599  indiscld  23066  cnindis  23267  connclo  23390  txindis  23609  xpsxmetlem  24354  xpsmet  24357  ishl2  25347  recnprss  25881  recnperf  25882  dvlip2  25972  coseq0negpitopi  26480  pythag  26794  reasinsin  26873  scvxcvx  26963  perfectlem2  27207  lgslem4  27277  lgseisenlem2  27353  2lgsoddprmlem3  27391  usgredg4  29300  konigsberg  30342  ex-pr  30515  elpreq  32613  1neg1t1neg1  32826  tocyc01  33194  drngidl  33508  drng0mxidl  33551  ply1dg3rt0irred  33659  rtelextdg2  33887  constrconj  33905  signswch  34721  kur14lem7  35410  poimirlem31  37986  ftc1anclem2  38029  wepwsolem  43488  omabs2  43778  omcl3g  43780  relexp01min  44158  clsk1indlem1  44490  mnuprdlem1  44717  mnuprdlem2  44718  mnuprdlem3  44719  mnurndlem1  44726  ssrecnpr  44753  seff  44754  sblpnf  44755  expgrowthi  44778  dvconstbi  44779  sumpair  45484  refsum2cnlem1  45486  iooinlbub  45949  cncfiooicclem1  46339  dvmptconst  46361  dvmptidg  46363  dvmulcncf  46371  dvdivcncf  46373  elprneb  47489  minusmodnep2tmod  47819  perfectALTVlem2  48210  grtriclwlk3  48433  gpgcubic  48567  gpg5nbgr3star  48569  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem7  48589  gpgprismgr4cycllem10  48592  pgnbgreunbgr  48613  0dig2pr01  49098  prelrrx2b  49202  infsubc  49547  infsubc2  49548  setc2othin  49953