Theorem pri1 2447

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 1474	. . 3 |- A = A
2	1	orci 270	. 2 |- (A = A \/ A = B)
3		pri1.1	. . 3 |- A e. V
4	3	elpr 2421	. 2 |- (A e. {A, B} <-> (A = A \/ A = B))
5	2, 4	mpbir 190	1 |- A e. {A, B}

Syntax hints:   \/ wo 222   = wceq 955   e. wcel 957  Vcvv 1808  {cpr 2407

This theorem is referenced by:  pri2 2448  tpi1 2452  prnz 2456  prss 2468  preqr1 2478  preq12b 2480  prel12 2481  opi1 2780  opth1 2782  opprc1b 2792  unisn2 2871  opeluu 2875  fr2nr 2921  dmrnssfld 3353  funopg 3543  2dom 4417  pw2en 4435  opthreg 4587  aceq6b 4725  brdom7disj 4787  brdom6disj 4788  pnfxr 5476  indistop 7608

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-un 2047  df-sn 2409  df-pr 2410

Copyright terms: Public domain