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 269	1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1536   ∈ wcel 2113  {cpr 4572

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-un 3944  df-sn 4571  df-pr 4573

This theorem is referenced by:  nelpri  4597  nelprd  4599  tppreqb  4741  elpreqpr  4800  elpr2elpr  4802  prproe  4839  3elpr2eq  4840  opth1  5370  0nelop  5389  ftpg  6921  2oconcl  8131  cantnflem2  9156  eldju1st  9355  m1expcl2  13454  hash2pwpr  13837  bitsinv1lem  15793  prm23lt5  16154  fnpr2ob  16834  fvprif  16837  xpsfeq  16839  pmtrprfval  18618  m1expaddsub  18629  psgnprfval  18652  frgpuptinv  18900  frgpup3lem  18906  simpgnsgeqd  19226  2nsgsimpgd  19227  simpgnsgbid  19228  cnmsgnsubg  20724  zrhpsgnelbas  20741  mdetralt  21220  m2detleiblem1  21236  indiscld  21702  cnindis  21903  connclo  22026  txindis  22245  xpsxmetlem  22992  xpsmet  22995  ishl2  23976  recnprss  24505  recnperf  24506  dvlip2  24595  coseq0negpitopi  25092  pythag  25398  reasinsin  25477  scvxcvx  25566  perfectlem2  25809  lgslem4  25879  lgseisenlem2  25955  2lgsoddprmlem3  25993  usgredg4  27002  konigsberg  28039  ex-pr  28212  elpreq  30293  1neg1t1neg1  30476  tocyc01  30764  signswch  31835  kur14lem7  32463  poimirlem31  34927  ftc1anclem2  34972  wepwsolem  39648  relexp01min  40064  clsk1indlem1  40401  mnuprdlem1  40614  mnuprdlem2  40615  mnuprdlem3  40616  mnurndlem1  40623  ssrecnpr  40646  seff  40647  sblpnf  40648  expgrowthi  40671  dvconstbi  40672  sumpair  41298  refsum2cnlem1  41300  iooinlbub  41782  elprn1  41920  elprn2  41921  cncfiooicclem1  42182  dvmptconst  42205  dvmptidg  42207  dvmulcncf  42216  dvdivcncf  42218  elprneb  43271  perfectALTVlem2  43894  0dig2pr01  44677  prelrrx2b  44708