Theorem elpri 4608

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2147  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  elprn1  4612  elprn2  4613  nelpri  4617  nelprd  4619  tppreqb  4770  elpreqpr  4827  elpr2elpr  4829  prproe  4838  3elpr2eq  4839  opth1  5451  0nelop  5475  ftpg  7192  fvf1pr  7346  2oconcl  8549  cantnflem2  9728  eldju1st  10041  m1expcl2  14268  hash2pwpr  14662  bitsinv1lem  16655  prm23lt5  17036  fnpr2ob  17780  fvprif  17783  xpsfeq  17785  ex-chn2  18862  pmtrprfval  19752  m1expaddsub  19763  psgnprfval  19786  frgpuptinv  20036  frgpup3lem  20042  simpgnsgeqd  20368  2nsgsimpgd  20369  simpgnsgbid  20370  drngidl  21590  cnmsgnsubg  21938  zrhpsgnelbas  21955  mdetralt  22978  m2detleiblem1  22994  indiscld  23464  cnindis  23665  connclo  23788  txindis  24008  xpsxmetlem  24753  xpsmet  24756  ishl2  25746  recnprss  26279  recnperf  26280  dvlip2  26370  coseq0negpitopi  26889  pythag  27202  reasinsin  27281  scvxcvx  27370  perfectlem2  27614  lgslem4  27684  lgseisenlem2  27760  2lgsoddprmlem3  27798  usgredg4  29855  konigsberg  30915  ex-pr  31088  elpreq  33223  1neg1t1neg1  33426  tocyc01  33778  drng0mxidl  34104  ply1dg3rt0irred  34219  rtelextdg2  34470  constrconj  34488  signswch  35301  kur14lem7  36185  poimirlem31  38837  ftc1anclem2  38880  wepwsolem  44315  omabs2  44595  omcl3g  44597  relexp01min  44974  clsk1indlem1  45306  mnuprdlem1  45517  mnuprdlem2  45518  mnuprdlem3  45519  mnurndlem1  45526  ssrecnpr  45553  seff  45554  sblpnf  45555  expgrowthi  45578  dvconstbi  45579  sumpair  46326  refsum2cnlem1  46328  iooinlbub  46786  cncfiooicclem1  47176  dvmptconst  47198  dvmptidg  47200  dvmulcncf  47208  dvdivcncf  47210  elprneb  48372  minusmodnep2tmod  48702  perfectALTVlem2  49093  grtriclwlk3  49316  gpgcubic  49450  gpg5nbgr3star  49452  gpgprismgr4cycllem3  49468  gpgprismgr4cycllem7  49472  gpgprismgr4cycllem10  49475  pgnbgreunbgr  49496  0dig2pr01  50053  infsubc  50505  infsubc2  50506  setc2othin  50932