Theorem elpri 3732

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720   = wceq 1402   ∈ wcel 2209  {cpr 3710

This proof depends on 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 proof 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 3715  df-pr 3716

This theorem is used by:  nelpri  3733  nelprd  3735  elpr2elpr  3901  opth1  4376  0nelop  4388  ontr2exmid  4672  onintexmid  4720  reg3exmidlemwe  4726  funtpg  5432  ftpg  5899  acexmidlemcase  6080  2oconcl  6712  el2oss1o  6716  pw2f1odclem  7134  en2eqpr  7214  2omap  7319  eldju1st  7412  nninfisol  7474  finomni  7481  exmidomniim  7482  ismkvnex  7496  nninfwlpoimlemginf  7517  pr2cv1  7542  exmidonfinlem  7546  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  sup3exmid  9290  m1expcl2  11013  maxleim  11988  maxleast  11996  zmaxcl  12007  minmax  12014  zmincl  12023  xrmaxleim  12029  xrmaxaddlem  12045  xrminmax  12050  bitsinv1lem  12747  nninfctlemfo  12836  prm23lt5  13065  unct  13385  fnpr2ob  13714  fvprif  13717  xpsfeq  13719  qtopbas  15714  limcimolemlt  15856  recnprss  15879  dvmptid  15908  dvmptc  15909  coseq0negpitopi  16029  perfectlem2  16261  lgslem4  16288  lgseisenlem2  16356  2lgslem3  16386  2lgsoddprmlem3  16396  usgredg4  16622  vdegp1aid  16721  konigsberg  16900  012of  17189  2o01f  17190  nninfalllem1  17217  nninfall  17218  nninfsellemqall  17224  nninfomnilem  17227  nnnninfex  17231  nninfnfiinf  17232  trilpolemclim  17252  trilpolemcl  17253  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  iswomni0  17268  nconstwlpolemgt0  17281  nconstwlpolem  17282