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\in \mathrm{V}$$
	cnvsn.2	$$⊢B\in \mathrm{V}$$
Assertion	op1sta	$$⊢\bigcup \mathrm{dom}\left\{⟨A,B⟩\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	$$⊢A\in \mathrm{V}$$
2		cnvsn.2	$$⊢B\in \mathrm{V}$$
3	2	dmsnop	$$⊢\mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$
4	3	unieqi	$$⊢\bigcup \mathrm{dom}\left\{⟨A,B⟩\right\}=\bigcup \left\{A\right\}$$
5	1	unisn	$$⊢\bigcup \left\{A\right\}=A$$
6	4 5	eqtri	$$⊢\bigcup \mathrm{dom}\left\{⟨A,B⟩\right\}=A$$