Theorem elpri 3612

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

Syntax hints:   → wi 4   ∨ wo 708   = wceq 1353   ∈ wcel 2146  {cpr 3590

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596

This theorem is referenced by:  nelpri  3613  nelprd  3615  opth1  4230  0nelop  4242  ontr2exmid  4518  onintexmid  4566  reg3exmidlemwe  4572  funtpg  5259  ftpg  5692  acexmidlemcase  5860  2oconcl  6430  el2oss1o  6434  en2eqpr  6897  eldju1st  7060  nninfisol  7121  finomni  7128  exmidomniim  7129  ismkvnex  7143  nninfwlpoimlemginf  7164  exmidonfinlem  7182  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  exmidaclem  7197  sup3exmid  8887  m1expcl2  10512  maxleim  11182  maxleast  11190  zmaxcl  11201  minmax  11206  xrmaxleim  11220  xrmaxaddlem  11236  xrminmax  11241  prm23lt5  12230  unct  12410  qtopbas  13593  limcimolemlt  13704  recnprss  13727  coseq0negpitopi  13828  lgslem4  13975  012of  14305  2o01f  14306  nninfalllem1  14318  nninfall  14319  nninfsellemqall  14325  nninfomnilem  14328  trilpolemclim  14345  trilpolemcl  14346  trilpolemisumle  14347  trilpolemeq1  14349  trilpolemlt1  14350  iswomni0  14360  nconstwlpolemgt0  14372  nconstwlpolem  14373