Theorem elpr 3990

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 3988	. 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 366   = wceq 1405   e. wcel 1842   _Vcvv 3059   {cpr 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-un 3419  df-sn 3973  df-pr 3975

This theorem is referenced by:  difprsnss  4107  preqr1  4146  preq12b  4148  prel12  4149  pwpr  4187  pwtp  4188  unipr  4204  intpr  4261  axpr  4629  zfpair2  4631  elop  4657  opthwiener  4692  tpres  6104  fnprb  6110  2oconcl  7190  pw2f1olem  7659  sdom2en01  8714  gruun  9214  fzpr  11790  m1expeven  12257  bpoly2  14002  bpoly3  14003  isprm2  14434  drngnidl  18197  psgninv  18916  psgnodpm  18922  mdetunilem7  19412  indistopon  19794  dfcon2  20212  cnconn  20215  uncon  20222  txindis  20427  txcon  20482  filcon  20676  xpsdsval  21176  rolle  22683  dvivthlem1  22701  ang180lem3  23470  ang180lem4  23471  wilthlem2  23724  sqff1o  23837  ppiub  23860  lgslem1  23952  lgsdir2lem4  23982  lgsdir2lem5  23983  usgraexmpl  24818  3vfriswmgralem  25421  signslema  29025  subfacp1lem1  29476  subfacp1lem4  29480  nosgnn0  30118  rankeq1o  30509  onsucconi  30669  topdifinfindis  31263  divrngidl  31707  isfldidl  31747  dihmeetlem2N  34319  wopprc  35334  pw2f1ocnv  35341  kelac2lem  35372  cncfiooicclem1  37064  elmod2OLD  37677  gsumpr  38461  nn0sumshdiglem2  38753