Theorem elpri 4615

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594

This theorem is used by:  elprn1  4619  elprn2  4620  nelpri  4623  nelprd  4625  tppreqb  4775  elpreqpr  4834  elpr2elpr  4836  prproe  4872  3elpr2eq  4873  opth1  5459  0nelop  5481  ftpg  7157  fvf1pr  7311  2oconcl  8490  cantnflem2  9662  eldju1st  9921  m1expcl2  14134  hash2pwpr  14526  bitsinv1lem  16516  prm23lt5  16891  fnpr2ob  17629  fvprif  17632  xpsfeq  17634  ex-chn2  18711  pmtrprfval  19580  m1expaddsub  19591  psgnprfval  19614  frgpuptinv  19864  frgpup3lem  19870  simpgnsgeqd  20196  2nsgsimpgd  20197  simpgnsgbid  20198  drngidl  21414  cnmsgnsubg  21756  zrhpsgnelbas  21773  mdetralt  22794  m2detleiblem1  22810  indiscld  23277  cnindis  23478  connclo  23601  txindis  23820  xpsxmetlem  24565  xpsmet  24568  ishl2  25558  recnprss  26092  recnperf  26093  dvlip2  26183  coseq0negpitopi  26697  pythag  27011  reasinsin  27090  scvxcvx  27179  perfectlem2  27423  lgslem4  27493  lgseisenlem2  27569  2lgsoddprmlem3  27607  usgredg4  29596  konigsberg  30637  ex-pr  30810  elpreq  32903  1neg1t1neg1  33112  tocyc01  33461  drng0mxidl  33781  ply1dg3rt0irred  33897  rtelextdg2  34140  constrconj  34158  signswch  34972  kur14lem7  35717  poimirlem31  38335  ftc1anclem2  38378  wepwsolem  43802  omabs2  44092  omcl3g  44094  relexp01min  44472  clsk1indlem1  44804  mnuprdlem1  45015  mnuprdlem2  45016  mnuprdlem3  45017  mnurndlem1  45024  ssrecnpr  45051  seff  45052  sblpnf  45053  expgrowthi  45076  dvconstbi  45077  sumpair  45788  refsum2cnlem1  45790  iooinlbub  46250  cncfiooicclem1  46640  dvmptconst  46662  dvmptidg  46664  dvmulcncf  46672  dvdivcncf  46674  elprneb  47799  minusmodnep2tmod  48129  perfectALTVlem2  48520  grtriclwlk3  48743  gpgcubic  48877  gpg5nbgr3star  48879  gpgprismgr4cycllem3  48895  gpgprismgr4cycllem7  48899  gpgprismgr4cycllem10  48902  pgnbgreunbgr  48923  0dig2pr01  49423  prelrrx2b  49527  infsubc  49871  infsubc2  49872  setc2othin  50277