Theorem elpri 3606

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

Syntax hints:   → wi 4   ∨ wo 703   = wceq 1348   ∈ wcel 2141  {cpr 3584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590

This theorem is referenced by:  nelpri  3607  nelprd  3609  opth1  4221  0nelop  4233  ontr2exmid  4509  onintexmid  4557  reg3exmidlemwe  4563  funtpg  5249  ftpg  5680  acexmidlemcase  5848  2oconcl  6418  el2oss1o  6422  en2eqpr  6885  eldju1st  7048  nninfisol  7109  finomni  7116  exmidomniim  7117  ismkvnex  7131  nninfwlpoimlemginf  7152  exmidonfinlem  7170  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  sup3exmid  8873  m1expcl2  10498  maxleim  11169  maxleast  11177  zmaxcl  11188  minmax  11193  xrmaxleim  11207  xrmaxaddlem  11223  xrminmax  11228  prm23lt5  12217  unct  12397  qtopbas  13316  limcimolemlt  13427  recnprss  13450  coseq0negpitopi  13551  lgslem4  13698  012of  14028  2o01f  14029  nninfalllem1  14041  nninfall  14042  nninfsellemqall  14048  nninfomnilem  14051  trilpolemclim  14068  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  iswomni0  14083  nconstwlpolemgt0  14095  nconstwlpolem  14096