Theorem op1stg

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

	Ref	Expression
Assertion	op1stg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		opeq1	⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
2	1	fveq2d	⊢ ( 𝑥 = 𝐴 → ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 1st ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
3		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
4	2 3	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥 ↔ ( 1st ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = 𝐴 ) )
5		opeq2	⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
6	5	fveqeq2d	⊢ ( 𝑦 = 𝐵 → ( ( 1st ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = 𝐴 ↔ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 ) )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	op1st	⊢ ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥
10	4 6 9	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )