Theorem elpri 4603

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  nelpri  4609  nelprd  4611  tppreqb  4759  elpreqpr  4821  elpr2elpr  4823  prproe  4859  3elpr2eq  4860  opth1  5422  0nelop  5443  ftpg  7094  fvf1pr  7248  2oconcl  8428  cantnflem2  9605  eldju1st  9838  m1expcl2  14010  hash2pwpr  14401  bitsinv1lem  16370  prm23lt5  16744  fnpr2ob  17480  fvprif  17483  xpsfeq  17485  pmtrprfval  19384  m1expaddsub  19395  psgnprfval  19418  frgpuptinv  19668  frgpup3lem  19674  simpgnsgeqd  20000  2nsgsimpgd  20001  simpgnsgbid  20002  cnmsgnsubg  21502  zrhpsgnelbas  21519  mdetralt  22511  m2detleiblem1  22527  indiscld  22994  cnindis  23195  connclo  23318  txindis  23537  xpsxmetlem  24283  xpsmet  24286  ishl2  25286  recnprss  25821  recnperf  25822  dvlip2  25916  coseq0negpitopi  26428  pythag  26743  reasinsin  26822  scvxcvx  26912  perfectlem2  27157  lgslem4  27227  lgseisenlem2  27303  2lgsoddprmlem3  27341  usgredg4  29180  konigsberg  30219  ex-pr  30392  elpreq  32490  1neg1t1neg1  32694  tocyc01  33073  drngidl  33383  drng0mxidl  33426  ply1dg3rt0irred  33530  rtelextdg2  33696  constrconj  33714  signswch  34531  kur14lem7  35187  poimirlem31  37633  ftc1anclem2  37676  wepwsolem  43018  omabs2  43308  omcl3g  43310  relexp01min  43689  clsk1indlem1  44021  mnuprdlem1  44248  mnuprdlem2  44249  mnuprdlem3  44250  mnurndlem1  44257  ssrecnpr  44284  seff  44285  sblpnf  44286  expgrowthi  44309  dvconstbi  44310  sumpair  45016  refsum2cnlem1  45018  iooinlbub  45486  elprn1  45618  elprn2  45619  cncfiooicclem1  45878  dvmptconst  45900  dvmptidg  45902  dvmulcncf  45910  dvdivcncf  45912  elprneb  47017  minusmodnep2tmod  47341  perfectALTVlem2  47710  grtriclwlk3  47933  gpgcubic  48067  gpg5nbgr3star  48069  gpgprismgr4cycllem3  48085  gpgprismgr4cycllem7  48089  gpgprismgr4cycllem10  48092  pgnbgreunbgr  48113  0dig2pr01  48599  prelrrx2b  48703  infsubc  49049  infsubc2  49050  setc2othin  49455