Theorem elpri 4671

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

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1537   ∈ wcel 2108  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  nelpri  4677  nelprd  4679  tppreqb  4830  elpreqpr  4891  elpr2elpr  4893  prproe  4929  3elpr2eq  4930  opth1  5495  0nelop  5515  ftpg  7190  fvf1pr  7343  2oconcl  8559  cantnflem2  9759  eldju1st  9992  m1expcl2  14136  hash2pwpr  14525  bitsinv1lem  16487  prm23lt5  16861  fnpr2ob  17618  fvprif  17621  xpsfeq  17623  pmtrprfval  19529  m1expaddsub  19540  psgnprfval  19563  frgpuptinv  19813  frgpup3lem  19819  simpgnsgeqd  20145  2nsgsimpgd  20146  simpgnsgbid  20147  cnmsgnsubg  21618  zrhpsgnelbas  21635  mdetralt  22635  m2detleiblem1  22651  indiscld  23120  cnindis  23321  connclo  23444  txindis  23663  xpsxmetlem  24410  xpsmet  24413  ishl2  25423  recnprss  25959  recnperf  25960  dvlip2  26054  coseq0negpitopi  26563  pythag  26878  reasinsin  26957  scvxcvx  27047  perfectlem2  27292  lgslem4  27362  lgseisenlem2  27438  2lgsoddprmlem3  27476  usgredg4  29252  konigsberg  30289  ex-pr  30462  elpreq  32558  1neg1t1neg1  32751  tocyc01  33111  drngidl  33426  drng0mxidl  33469  ply1dg3rt0irred  33572  rtelextdg2  33718  constrconj  33735  signswch  34538  kur14lem7  35180  poimirlem31  37611  ftc1anclem2  37654  wepwsolem  42999  omabs2  43294  omcl3g  43296  relexp01min  43675  clsk1indlem1  44007  mnuprdlem1  44241  mnuprdlem2  44242  mnuprdlem3  44243  mnurndlem1  44250  ssrecnpr  44277  seff  44278  sblpnf  44279  expgrowthi  44302  dvconstbi  44303  sumpair  44935  refsum2cnlem1  44937  iooinlbub  45419  elprn1  45554  elprn2  45555  cncfiooicclem1  45814  dvmptconst  45836  dvmptidg  45838  dvmulcncf  45846  dvdivcncf  45848  elprneb  46944  perfectALTVlem2  47596  grtriclwlk3  47796  0dig2pr01  48344  prelrrx2b  48448  setc2othin  48723