Theorem op1sta

Description: Extract the first member of an ordered pair. (See op2nda to extract the second member, op1stb for an alternate version, and op1st for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003)

	Ref	Expression
Hypotheses	cnvsn.1	|- A e. _V
	cnvsn.2	|- B e. _V
Assertion	op1sta	|- U. dom { <. A , B >. } = A

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	|- A e. _V
2		cnvsn.2	|- B e. _V
3	2	dmsnop	|- dom { <. A , B >. } = { A }
4	3	unieqi	|- U. dom { <. A , B >. } = U. { A }
5	1	unisn	|- U. { A } = A
6	4 5	eqtri	|- U. dom { <. A , B >. } = A