Theorem pri1 2441

Description: One of the two elements of an unordered pair. Part of Theorem 7.6 of [Quine] p. 49.

Hypothesis

Ref	Expression
pri1.1	|- A e. V

Assertion

Ref	Expression
pri1	|- A e. {A, B}

Proof of Theorem pri1

Step	Hyp	Ref	Expression
1		eqid 1468	. . 3 |- A = A
2	1	orci 270	. 2 |- (A = A \/ A = B)
3		pri1.1	. . 3 |- A e. V
4	3	elpr 2414	. 2 |- (A e. {A, B} <-> (A = A \/ A = B))
5	2, 4	mpbir 190	1 |- A e. {A, B}

Syntax hints:   \/ wo 222   = wceq 953   e. wcel 955  Vcvv 1802  {cpr 2400

This theorem is referenced by:  pri2 2442  tpi1 2446  prnz 2450  prss 2462  preqr1 2472  preq12b 2474  prel12 2475  opi1 2774  opth1 2776  opprc1b 2786  unisn2 2866  opeluu 2869  fr2nr 2915  dmrnssfld 3343  funopg 3533  2dom 4408  pw2en 4426  opthreg 4576  aceq6b 4714  brdom7disj 4776  brdom6disj 4777  pnfxr 5465  indistop 7590

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403

Copyright terms: Public domain