Theorem op1stg

Description: Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005)

	Ref	Expression
Assertion	op1stg	$$⊢\left(A\in V\wedge B\in W\right)\to 1^{st}\left(⟨A,B⟩\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		opeq1	$$⊢x=A\to ⟨x,y⟩=⟨A,y⟩$$
2	1	fveq2d	$$⊢x=A\to 1^{st}\left(⟨x,y⟩\right)=1^{st}\left(⟨A,y⟩\right)$$
3		id	$$⊢x=A\to x=A$$
4	2 3	eqeq12d	$$⊢x=A\to \left(1^{st}\left(⟨x,y⟩\right)=x\leftrightarrow 1^{st}\left(⟨A,y⟩\right)=A\right)$$
5		opeq2	$$⊢y=B\to ⟨A,y⟩=⟨A,B⟩$$
6	5	fveqeq2d	$$⊢y=B\to \left(1^{st}\left(⟨A,y⟩\right)=A\leftrightarrow 1^{st}\left(⟨A,B⟩\right)=A\right)$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	op1st	$$⊢1^{st}\left(⟨x,y⟩\right)=x$$
10	4 6 9	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to 1^{st}\left(⟨A,B⟩\right)=A$$