Theorem elpri 3728

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

Syntax hints:   → wi 4   ∨ wo 720   = wceq 1402   ∈ wcel 2209  {cpr 3706

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712

This theorem is referenced by:  nelpri  3729  nelprd  3731  elpr2elpr  3896  opth1  4371  0nelop  4383  ontr2exmid  4667  onintexmid  4715  reg3exmidlemwe  4721  funtpg  5427  ftpg  5890  acexmidlemcase  6070  2oconcl  6702  el2oss1o  6706  pw2f1odclem  7124  en2eqpr  7204  2omap  7308  eldju1st  7401  nninfisol  7463  finomni  7470  exmidomniim  7471  ismkvnex  7485  nninfwlpoimlemginf  7506  pr2cv1  7531  exmidonfinlem  7535  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  sup3exmid  9277  m1expcl2  10976  maxleim  11949  maxleast  11957  zmaxcl  11968  minmax  11974  xrmaxleim  11988  xrmaxaddlem  12004  xrminmax  12009  bitsinv1lem  12706  nninfctlemfo  12795  prm23lt5  13020  unct  13311  fnpr2ob  13638  fvprif  13641  xpsfeq  13643  qtopbas  15546  limcimolemlt  15688  recnprss  15711  dvmptid  15740  dvmptc  15741  coseq0negpitopi  15860  perfectlem2  16028  lgslem4  16036  lgseisenlem2  16104  2lgslem3  16134  2lgsoddprmlem3  16144  usgredg4  16370  vdegp1aid  16469  konigsberg  16648  012of  16937  2o01f  16938  nninfalllem1  16956  nninfall  16957  nninfsellemqall  16963  nninfomnilem  16966  nnnninfex  16970  nninfnfiinf  16971  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  iswomni0  17006  nconstwlpolemgt0  17019  nconstwlpolem  17020