Theorem elpr 3998

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 3996	. 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 189   \/ wo 374   = wceq 1455   e. wcel 1898   _Vcvv 3057   {cpr 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-sn 3981  df-pr 3983

This theorem is referenced by:  difprsnss  4120  preqr1OLD  4162  preq12b  4164  prel12  4165  pwpr  4208  pwtp  4209  unipr  4225  intpr  4282  axpr  4655  zfpair2  4657  elopOLD  4685  opthwiener  4720  tpres  6146  fnprb  6152  2oconcl  7236  pw2f1olem  7707  sdom2en01  8763  gruun  9262  fzpr  11886  m1expeven  12357  bpoly2  14165  bpoly3  14166  lcmfpr  14655  isprm2  14687  drngnidl  18508  psgninv  19205  psgnodpm  19211  mdetunilem7  19698  indistopon  20071  dfcon2  20489  cnconn  20492  uncon  20499  txindis  20704  txcon  20759  filcon  20953  xpsdsval  21451  rolle  22998  dvivthlem1  23016  ang180lem3  23796  ang180lem4  23797  wilthlem2  24050  sqff1o  24165  ppiub  24188  lgslem1  24280  lgsdir2lem4  24310  lgsdir2lem5  24311  usgraexmplef  25184  3vfriswmgralem  25788  lmat22lem  28694  signslema  29501  subfacp1lem1  29952  subfacp1lem4  29956  nosgnn0  30595  rankeq1o  30988  onsucconi  31147  topdifinfindis  31795  poimirlem9  31995  divrngidl  32307  isfldidl  32347  dihmeetlem2N  34913  wopprc  35931  pw2f1ocnv  35938  kelac2lem  35968  rnmptpr  37498  cncfiooicclem1  37857  elmod2OLD  38861  structiedg0val  39266  gsumpr  40511  nn0sumshdiglem2  40802