Theorem op1stb

Description: Extract the first member of an ordered pair. Theorem 73 of Suppes p. 42. (See op2ndb to extract the second member, op1sta for an alternate version, and op1st for the preferred version.) (Contributed by NM, 25-Nov-2003)

	Ref	Expression
Hypotheses	op1stb.1	|- A e. _V
	op1stb.2	|- B e. _V
Assertion	op1stb	|- |^| |^| <. A , B >. = A

Proof

Step	Hyp	Ref	Expression
1		op1stb.1	|- A e. _V
2		op1stb.2	|- B e. _V
3	1 2	dfop	|- <. A , B >. = { { A } , { A , B } }
4	3	inteqi	|- |^| <. A , B >. = |^| { { A } , { A , B } }
5		snex	|- { A } e. _V
6		prex	|- { A , B } e. _V
7	5 6	intpr	|- |^| { { A } , { A , B } } = ( { A } i^i { A , B } )
8		snsspr1	|- { A } C_ { A , B }
9		df-ss	|- ( { A } C_ { A , B } <-> ( { A } i^i { A , B } ) = { A } )
10	8 9	mpbi	|- ( { A } i^i { A , B } ) = { A }
11	7 10	eqtri	|- |^| { { A } , { A , B } } = { A }
12	4 11	eqtri	|- |^| <. A , B >. = { A }
13	12	inteqi	|- |^| |^| <. A , B >. = |^| { A }
14	1	intsn	|- |^| { A } = A
15	13 14	eqtri	|- |^| |^| <. A , B >. = A