Theorem elpri 4649

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1540   ∈ wcel 2108  {cpr 4628

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629

This theorem is referenced by:  nelpri  4655  nelprd  4657  tppreqb  4805  elpreqpr  4867  elpr2elpr  4869  prproe  4905  3elpr2eq  4906  opth1  5480  0nelop  5501  ftpg  7176  fvf1pr  7327  2oconcl  8541  cantnflem2  9730  eldju1st  9963  m1expcl2  14126  hash2pwpr  14515  bitsinv1lem  16478  prm23lt5  16852  fnpr2ob  17603  fvprif  17606  xpsfeq  17608  pmtrprfval  19505  m1expaddsub  19516  psgnprfval  19539  frgpuptinv  19789  frgpup3lem  19795  simpgnsgeqd  20121  2nsgsimpgd  20122  simpgnsgbid  20123  cnmsgnsubg  21595  zrhpsgnelbas  21612  mdetralt  22614  m2detleiblem1  22630  indiscld  23099  cnindis  23300  connclo  23423  txindis  23642  xpsxmetlem  24389  xpsmet  24392  ishl2  25404  recnprss  25939  recnperf  25940  dvlip2  26034  coseq0negpitopi  26545  pythag  26860  reasinsin  26939  scvxcvx  27029  perfectlem2  27274  lgslem4  27344  lgseisenlem2  27420  2lgsoddprmlem3  27458  usgredg4  29234  konigsberg  30276  ex-pr  30449  elpreq  32548  1neg1t1neg1  32748  tocyc01  33138  drngidl  33461  drng0mxidl  33504  ply1dg3rt0irred  33607  rtelextdg2  33768  constrconj  33786  signswch  34576  kur14lem7  35217  poimirlem31  37658  ftc1anclem2  37701  wepwsolem  43054  omabs2  43345  omcl3g  43347  relexp01min  43726  clsk1indlem1  44058  mnuprdlem1  44291  mnuprdlem2  44292  mnuprdlem3  44293  mnurndlem1  44300  ssrecnpr  44327  seff  44328  sblpnf  44329  expgrowthi  44352  dvconstbi  44353  sumpair  45040  refsum2cnlem1  45042  iooinlbub  45514  elprn1  45648  elprn2  45649  cncfiooicclem1  45908  dvmptconst  45930  dvmptidg  45932  dvmulcncf  45940  dvdivcncf  45942  elprneb  47041  minusmodnep2tmod  47355  perfectALTVlem2  47709  grtriclwlk3  47912  gpgcubic  48035  gpg5nbgr3star  48037  0dig2pr01  48531  prelrrx2b  48635  setc2othin  49113