Theorem elpr 3792

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 3791	. 2 |- ( A e. _V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
3	1, 2	ax-mp 8	1 |- ( A e. { B , C } <-> ( A = B \/ A = C ) )

Syntax hints:   <-> wb 177   \/ wo 358   = wceq 1649   e. wcel 1721   _Vcvv 2916   {cpr 3775

This theorem is referenced by:  difprsnss  3894  preqr1  3932  preq12b  3934  prel12  3935  pwpr  3971  pwtp  3972  unipr  3989  intpr  4043  axpr  4362  zfpair2  4364  elop  4389  opthwiener  4418  xpsspw  4945  fnpr  5909  fnprOLD  5910  2oconcl  6706  pw2f1olem  7171  sdom2en01  8138  gruun  8637  renfdisj  9094  fzpr  11057  isprm2  13042  drngnidl  16255  indistopon  17020  dfcon2  17435  cnconn  17438  uncon  17445  txindis  17619  txcon  17674  filcon  17868  xpsdsval  18364  rolle  19827  dvivthlem1  19845  ang180lem3  20606  ang180lem4  20607  wilthlem2  20805  sqff1o  20918  ppiub  20941  perfectlem2  20967  lgslem1  21033  lgsdir2lem4  21063  lgsdir2lem5  21064  usgraexmpl  21373  subfacp1lem1  24818  subfacp1lem4  24822  m1expevenALT  24858  nosgnn0  25526  bpoly2  26007  bpoly3  26008  rankeq1o  26016  onsucconi  26091  divrngidl  26528  isfldidl  26568  wopprc  26991  pw2f1ocnv  26998  kelac2lem  27030  3vfriswmgralem  28108  dihmeetlem2N  31782

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-sn 3780  df-pr 3781