Theorem op1st

Description: Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004)

	Ref	Expression
Hypotheses	op1st.1	$$⊢A\in \mathrm{V}$$
	op1st.2	$$⊢B\in \mathrm{V}$$
Assertion	op1st	$$⊢1^{st}\left(⟨A,B⟩\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		op1st.1	$$⊢A\in \mathrm{V}$$
2		op1st.2	$$⊢B\in \mathrm{V}$$
3		1stval	$$⊢1^{st}\left(⟨A,B⟩\right)=\bigcup \mathrm{dom}\left\{⟨A,B⟩\right\}$$
4	1 2	op1sta	$$⊢\bigcup \mathrm{dom}\left\{⟨A,B⟩\right\}=A$$
5	3 4	eqtri	$$⊢1^{st}\left(⟨A,B⟩\right)=A$$