Theorem elpri 3661

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

Syntax hints:   → wi 4   ∨ wo 710   = wceq 1373   ∈ wcel 2177  {cpr 3639

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645

This theorem is referenced by:  nelpri  3662  nelprd  3664  opth1  4288  0nelop  4300  ontr2exmid  4581  onintexmid  4629  reg3exmidlemwe  4635  funtpg  5334  ftpg  5781  acexmidlemcase  5952  2oconcl  6538  el2oss1o  6542  pw2f1odclem  6946  en2eqpr  7019  eldju1st  7188  nninfisol  7250  finomni  7257  exmidomniim  7258  ismkvnex  7272  nninfwlpoimlemginf  7293  exmidonfinlem  7317  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  exmidaclem  7336  sup3exmid  9050  m1expcl2  10728  maxleim  11591  maxleast  11599  zmaxcl  11610  minmax  11616  xrmaxleim  11630  xrmaxaddlem  11646  xrminmax  11651  bitsinv1lem  12347  nninfctlemfo  12436  prm23lt5  12661  unct  12888  fnpr2ob  13247  fvprif  13250  xpsfeq  13252  qtopbas  15069  limcimolemlt  15211  recnprss  15234  dvmptid  15263  dvmptc  15264  coseq0negpitopi  15383  perfectlem2  15547  lgslem4  15555  lgseisenlem2  15623  2lgslem3  15653  2lgsoddprmlem3  15663  012of  16069  2o01f  16070  2omap  16071  nninfalllem1  16086  nninfall  16087  nninfsellemqall  16093  nninfomnilem  16096  nnnninfex  16100  nninfnfiinf  16101  trilpolemclim  16116  trilpolemcl  16117  trilpolemisumle  16118  trilpolemeq1  16120  trilpolemlt1  16121  iswomni0  16131  nconstwlpolemgt0  16144  nconstwlpolem  16145