Theorem pri2 2447

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 2446	. 2 |- B e. {B, A}
3		prcom 2443	. 2 |- {B, A} = {A, B}
4	2, 3	eleqtr 1543	1 |- B e. {A, B}

Syntax hints:   e. wcel 956  Vcvv 1807  {cpr 2406

This theorem is referenced by:  tpi2 2452  prss 2467  prel12 2480  opi2 2780  opthwiener 2802  opeluu 2874  fr2nr 2920  dmrnssfld 3351  funopg 3539  2dom 4414  pw2en 4432  aceq6b 4722  brdom7disj 4784  brdom6disj 4785  mnfxr 5474  indistop 7598

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409

Copyright terms: Public domain