Theorem elpr 3916

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 3914	. 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 1369   e. wcel 1756   _Vcvv 2993   {cpr 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-un 3354  df-sn 3899  df-pr 3901

This theorem is referenced by:  difprsnss  4030  preqr1  4067  preq12b  4069  prel12  4070  pwpr  4108  pwtp  4109  unipr  4125  intpr  4182  axpr  4551  zfpair2  4553  elop  4579  opthwiener  4614  xpsspw  4974  fnprb  5957  fnprOLD  5958  2oconcl  6964  pw2f1olem  7436  sdom2en01  8492  gruun  8994  renfdisj  9458  fzpr  11532  isprm2  13792  drngnidl  17333  psgninv  18034  psgnodpm  18040  mdetunilem7  18446  indistopon  18627  dfcon2  19045  cnconn  19048  uncon  19055  txindis  19229  txcon  19284  filcon  19478  xpsdsval  19978  rolle  21484  dvivthlem1  21502  ang180lem3  22229  ang180lem4  22230  wilthlem2  22429  sqff1o  22542  ppiub  22565  perfectlem2  22591  lgslem1  22657  lgsdir2lem4  22687  lgsdir2lem5  22688  usgraexmpl  23341  signslema  26985  subfacp1lem1  27089  subfacp1lem4  27093  m1expevenALT  27129  nosgnn0  27821  bpoly2  28222  bpoly3  28223  rankeq1o  28231  onsucconi  28305  divrngidl  28854  isfldidl  28894  wopprc  29405  pw2f1ocnv  29412  kelac2lem  29443  3vfriswmgralem  30622  gsumpr  30787  dihmeetlem2N  35040