Theorem elpri 4591

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  elprn1  4595  elprn2  4596  nelpri  4599  nelprd  4601  tppreqb  4750  elpreqpr  4810  elpr2elpr  4812  prproe  4848  3elpr2eq  4849  opth1  5428  0nelop  5450  ftpg  7110  fvf1pr  7262  2oconcl  8438  cantnflem2  9611  eldju1st  9847  m1expcl2  14047  hash2pwpr  14438  bitsinv1lem  16410  prm23lt5  16785  fnpr2ob  17522  fvprif  17525  xpsfeq  17527  ex-chn2  18604  pmtrprfval  19462  m1expaddsub  19473  psgnprfval  19496  frgpuptinv  19746  frgpup3lem  19752  simpgnsgeqd  20078  2nsgsimpgd  20079  simpgnsgbid  20080  cnmsgnsubg  21557  zrhpsgnelbas  21574  mdetralt  22573  m2detleiblem1  22589  indiscld  23056  cnindis  23257  connclo  23380  txindis  23599  xpsxmetlem  24344  xpsmet  24347  ishl2  25337  recnprss  25871  recnperf  25872  dvlip2  25962  coseq0negpitopi  26467  pythag  26781  reasinsin  26860  scvxcvx  26949  perfectlem2  27193  lgslem4  27263  lgseisenlem2  27339  2lgsoddprmlem3  27377  usgredg4  29286  konigsberg  30327  ex-pr  30500  elpreq  32598  1neg1t1neg1  32811  tocyc01  33179  drngidl  33493  drng0mxidl  33536  ply1dg3rt0irred  33644  rtelextdg2  33871  constrconj  33889  signswch  34705  kur14lem7  35394  poimirlem31  37972  ftc1anclem2  38015  wepwsolem  43470  omabs2  43760  omcl3g  43762  relexp01min  44140  clsk1indlem1  44472  mnuprdlem1  44699  mnuprdlem2  44700  mnuprdlem3  44701  mnurndlem1  44708  ssrecnpr  44735  seff  44736  sblpnf  44737  expgrowthi  44760  dvconstbi  44761  sumpair  45466  refsum2cnlem1  45468  iooinlbub  45931  cncfiooicclem1  46321  dvmptconst  46343  dvmptidg  46345  dvmulcncf  46353  dvdivcncf  46355  elprneb  47477  minusmodnep2tmod  47807  perfectALTVlem2  48198  grtriclwlk3  48421  gpgcubic  48555  gpg5nbgr3star  48557  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem10  48580  pgnbgreunbgr  48601  0dig2pr01  49086  prelrrx2b  49190  infsubc  49535  infsubc2  49536  setc2othin  49941