Theorem elpr 3892

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 3890	. 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 1364   e. wcel 1761   _Vcvv 2970   {cpr 3876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-un 3330  df-sn 3875  df-pr 3877

This theorem is referenced by:  difprsnss  4006  preqr1  4043  preq12b  4045  prel12  4046  pwpr  4084  pwtp  4085  unipr  4101  intpr  4158  axpr  4527  zfpair2  4529  elop  4555  opthwiener  4590  xpsspw  4949  fnprb  5933  fnprOLD  5934  2oconcl  6939  pw2f1olem  7411  sdom2en01  8467  gruun  8969  renfdisj  9433  fzpr  11507  isprm2  13767  drngnidl  17289  psgninv  17971  psgnodpm  17977  mdetunilem7  18383  indistopon  18564  dfcon2  18982  cnconn  18985  uncon  18992  txindis  19166  txcon  19221  filcon  19415  xpsdsval  19915  rolle  21421  dvivthlem1  21439  ang180lem3  22166  ang180lem4  22167  wilthlem2  22366  sqff1o  22479  ppiub  22502  perfectlem2  22528  lgslem1  22594  lgsdir2lem4  22624  lgsdir2lem5  22625  usgraexmpl  23254  signslema  26893  subfacp1lem1  26997  subfacp1lem4  27001  m1expevenALT  27037  nosgnn0  27728  bpoly2  28129  bpoly3  28130  rankeq1o  28138  onsucconi  28213  divrngidl  28753  isfldidl  28793  wopprc  29304  pw2f1ocnv  29311  kelac2lem  29342  3vfriswmgralem  30521  gsumpr  30675  dihmeetlem2N  34666