Theorem pri2 2442

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

Hypothesis

Ref	Expression
pri2.1	|- B e. V

Assertion

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

Proof of Theorem pri2

Step	Hyp	Ref	Expression
1		pri2.1	. . 3 |- B e. V
2	1	pri1 2441	. 2 |- B e. {B, A}
3		prcom 2437	. 2 |- {B, A} = {A, B}
4	2, 3	eleqtr 1538	1 |- B e. {A, B}

Syntax hints:   e. wcel 955  Vcvv 1802  {cpr 2400

This theorem is referenced by:  tpi2 2447  prss 2462  prel12 2475  opi2 2775  opthwiener 2796  opeluu 2869  fr2nr 2915  dmrnssfld 3343  funopg 3533  2dom 4408  pw2en 4426  aceq6b 4714  brdom7disj 4776  brdom6disj 4777  mnfxr 5466  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