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 2145  {cpr 4586

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  elprn1  4612  elprn2  4613  nelpri  4616  nelprd  4618  tppreqb  4768  elpreqpr  4827  elpr2elpr  4829  prproe  4865  3elpr2eq  4866  opth1  5444  0nelop  5468  ftpg  7158  fvf1pr  7313  2oconcl  8504  cantnflem2  9684  eldju1st  9997  m1expcl2  14221  hash2pwpr  14614  bitsinv1lem  16604  prm23lt5  16985  fnpr2ob  17723  fvprif  17726  xpsfeq  17728  ex-chn2  18805  pmtrprfval  19694  m1expaddsub  19705  psgnprfval  19728  frgpuptinv  19978  frgpup3lem  19984  simpgnsgeqd  20310  2nsgsimpgd  20311  simpgnsgbid  20312  drngidl  21532  cnmsgnsubg  21876  zrhpsgnelbas  21893  mdetralt  22916  m2detleiblem1  22932  indiscld  23402  cnindis  23603  connclo  23726  txindis  23946  xpsxmetlem  24691  xpsmet  24694  ishl2  25684  recnprss  26217  recnperf  26218  dvlip2  26308  coseq0negpitopi  26825  pythag  27138  reasinsin  27217  scvxcvx  27306  perfectlem2  27550  lgslem4  27620  lgseisenlem2  27696  2lgsoddprmlem3  27734  usgredg4  29791  konigsberg  30851  ex-pr  31024  elpreq  33117  1neg1t1neg1  33323  tocyc01  33672  drng0mxidl  33993  ply1dg3rt0irred  34109  rtelextdg2  34352  constrconj  34370  signswch  35183  kur14lem7  35956  poimirlem31  38549  ftc1anclem2  38592  wepwsolem  44028  omabs2  44318  omcl3g  44320  relexp01min  44698  clsk1indlem1  45030  mnuprdlem1  45241  mnuprdlem2  45242  mnuprdlem3  45243  mnurndlem1  45250  ssrecnpr  45277  seff  45278  sblpnf  45279  expgrowthi  45302  dvconstbi  45303  sumpair  46021  refsum2cnlem1  46023  iooinlbub  46482  cncfiooicclem1  46872  dvmptconst  46894  dvmptidg  46896  dvmulcncf  46904  dvdivcncf  46906  elprneb  48068  minusmodnep2tmod  48398  perfectALTVlem2  48789  grtriclwlk3  49012  gpgcubic  49146  gpg5nbgr3star  49148  gpgprismgr4cycllem3  49164  gpgprismgr4cycllem7  49168  gpgprismgr4cycllem10  49171  pgnbgreunbgr  49192  0dig2pr01  49691  prelrrx2b  49795  infsubc  50137  infsubc2  50138  setc2othin  50543