Theorem elpr 4045

Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)

Hypothesis

Ref	Expression
elpr.1	|- A e. _V

Assertion

Ref	Expression
elpr	|- ( A e. { B , C } <-> ( A = B \/ A = C ) )

Proof of Theorem elpr

Step	Hyp	Ref	Expression
1		elpr.1	. 2 |- A e. _V
2		elprg 4043	. 2 |- ( A e. _V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
3	1, 2	ax-mp 5	1 |- ( A e. { B , C } <-> ( A = B \/ A = C ) )

Syntax hints:   <-> wb 184   \/ wo 368   = wceq 1379   e. wcel 1767   _Vcvv 3113   {cpr 4029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030

This theorem is referenced by:  difprsnss  4162  preqr1  4200  preq12b  4202  prel12  4203  pwpr  4241  pwtp  4242  unipr  4258  intpr  4315  axpr  4685  zfpair2  4687  elop  4713  opthwiener  4749  xpsspw  5116  fnprb  6120  fnprOLD  6121  2oconcl  7154  pw2f1olem  7622  sdom2en01  8683  gruun  9185  renfdisj  9648  fzpr  11736  isprm2  14087  drngnidl  17688  psgninv  18425  psgnodpm  18431  mdetunilem7  18927  indistopon  19308  dfcon2  19726  cnconn  19729  uncon  19736  txindis  19962  txcon  20017  filcon  20211  xpsdsval  20711  rolle  22218  dvivthlem1  22236  ang180lem3  22968  ang180lem4  22969  wilthlem2  23168  sqff1o  23281  ppiub  23304  perfectlem2  23330  lgslem1  23396  lgsdir2lem4  23426  lgsdir2lem5  23427  usgraexmpl  24174  3vfriswmgralem  24777  signslema  28270  subfacp1lem1  28374  subfacp1lem4  28378  m1expevenALT  28414  nosgnn0  29271  bpoly2  29672  bpoly3  29673  rankeq1o  29681  onsucconi  29755  divrngidl  30255  isfldidl  30295  wopprc  30803  pw2f1ocnv  30810  kelac2lem  30841  cncfiooicclem1  31459  gsumpr  32245  dihmeetlem2N  36313