Theorem elpri 3646

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

Syntax hints:   → wi 4   ∨ wo 709   = wceq 1364   ∈ wcel 2167  {cpr 3624

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630

This theorem is referenced by:  nelpri  3647  nelprd  3649  opth1  4270  0nelop  4282  ontr2exmid  4562  onintexmid  4610  reg3exmidlemwe  4616  funtpg  5310  ftpg  5749  acexmidlemcase  5920  2oconcl  6506  el2oss1o  6510  pw2f1odclem  6904  en2eqpr  6977  eldju1st  7146  nninfisol  7208  finomni  7215  exmidomniim  7216  ismkvnex  7230  nninfwlpoimlemginf  7251  exmidonfinlem  7272  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidaclem  7291  sup3exmid  9001  m1expcl2  10670  maxleim  11387  maxleast  11395  zmaxcl  11406  minmax  11412  xrmaxleim  11426  xrmaxaddlem  11442  xrminmax  11447  bitsinv1lem  12143  nninfctlemfo  12232  prm23lt5  12457  unct  12684  fnpr2ob  13042  fvprif  13045  xpsfeq  13047  qtopbas  14842  limcimolemlt  14984  recnprss  15007  dvmptid  15036  dvmptc  15037  coseq0negpitopi  15156  perfectlem2  15320  lgslem4  15328  lgseisenlem2  15396  2lgslem3  15426  2lgsoddprmlem3  15436  012of  15724  2o01f  15725  2omap  15726  nninfalllem1  15739  nninfall  15740  nninfsellemqall  15746  nninfomnilem  15749  trilpolemclim  15767  trilpolemcl  15768  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  iswomni0  15782  nconstwlpolemgt0  15795  nconstwlpolem  15796