Theorem elpr 3690

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 3689	. 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 105   \/ wo 715   = wceq 1397   e. wcel 2202   _Vcvv 2802   {cpr 3670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676

This theorem is referenced by:  prmg  3794  difprsnss  3811  preqr1  3851  preq12b  3853  prel12  3854  pwprss  3889  pwtpss  3890  unipr  3907  intpr  3960  zfpair2  4300  elop  4323  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  en2lp  4652  reg3exmidlemwe  4677  xpsspw  4838  acexmidlem2  6014  2oconcl  6606  exmidpw  7099  exmidpweq  7100  renfdisj  8238  fzpr  10311  maxabslemval  11768  xrmaxiflemval  11810  isprm2  12688  2lgslem4  15831  structiedg0val  15890  bj-zfpair2  16505  ss1oel2o  16586