Theorem elpr 4050

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 4048	. 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 1395   e. wcel 1819   _Vcvv 3109   {cpr 4034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476  df-sn 4033  df-pr 4035

This theorem is referenced by:  difprsnss  4167  preqr1  4206  preq12b  4208  prel12  4209  pwpr  4247  pwtp  4248  unipr  4264  intpr  4322  axpr  4694  zfpair2  4696  elop  4722  opthwiener  4758  xpsspw  5125  tpres  6125  fnprb  6131  2oconcl  7171  pw2f1olem  7640  sdom2en01  8699  gruun  9201  fzpr  11760  isprm2  14236  drngnidl  18003  psgninv  18744  psgnodpm  18750  mdetunilem7  19246  indistopon  19628  dfcon2  20045  cnconn  20048  uncon  20055  txindis  20260  txcon  20315  filcon  20509  xpsdsval  21009  rolle  22516  dvivthlem1  22534  ang180lem3  23268  ang180lem4  23269  wilthlem2  23468  sqff1o  23581  ppiub  23604  lgslem1  23696  lgsdir2lem4  23726  lgsdir2lem5  23727  usgraexmpl  24527  3vfriswmgralem  25130  signslema  28694  subfacp1lem1  28798  subfacp1lem4  28802  m1expevenALT  28838  nosgnn0  29592  bpoly2  29981  bpoly3  29982  rankeq1o  29990  onsucconi  30064  divrngidl  30587  isfldidl  30627  wopprc  31134  pw2f1ocnv  31141  kelac2lem  31172  cncfiooicclem1  31857  gsumpr  33052  dihmeetlem2N  37127