Theorem elpri 3712

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

Syntax hints:   → wi 4   ∨ wo 716   = wceq 1398   ∈ wcel 2203  {cpr 3690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696

This theorem is referenced by:  nelpri  3713  nelprd  3715  elpr2elpr  3880  opth1  4352  0nelop  4364  ontr2exmid  4647  onintexmid  4695  reg3exmidlemwe  4701  funtpg  5407  ftpg  5868  acexmidlemcase  6045  2oconcl  6672  el2oss1o  6676  pw2f1odclem  7087  en2eqpr  7167  2omap  7269  eldju1st  7362  nninfisol  7424  finomni  7431  exmidomniim  7432  ismkvnex  7446  nninfwlpoimlemginf  7467  pr2cv1  7492  exmidonfinlem  7496  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidaclem  7515  sup3exmid  9231  m1expcl2  10923  maxleim  11890  maxleast  11898  zmaxcl  11909  minmax  11915  xrmaxleim  11929  xrmaxaddlem  11945  xrminmax  11950  bitsinv1lem  12647  nninfctlemfo  12736  prm23lt5  12961  unct  13193  fnpr2ob  13553  fvprif  13556  xpsfeq  13558  qtopbas  15387  limcimolemlt  15529  recnprss  15552  dvmptid  15581  dvmptc  15582  coseq0negpitopi  15701  perfectlem2  15868  lgslem4  15876  lgseisenlem2  15944  2lgslem3  15974  2lgsoddprmlem3  15984  usgredg4  16210  vdegp1aid  16309  konigsberg  16488  012of  16767  2o01f  16768  nninfalllem1  16786  nninfall  16787  nninfsellemqall  16793  nninfomnilem  16796  nnnninfex  16800  nninfnfiinf  16801  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  iswomni0  16836  nconstwlpolemgt0  16850  nconstwlpolem  16851