Metamath Proof Explorer


Theorem 1stval2

Description: Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of Monk1 p. 52. (Contributed by NM, 18-Aug-2006)

Ref Expression
Assertion 1stval2 ( 𝐴 ∈ ( V × V ) → ( 1st𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 elvv ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
2 vex 𝑥 ∈ V
3 vex 𝑦 ∈ V
4 2 3 op1st ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥
5 2 3 op1stb 𝑥 , 𝑦 ⟩ = 𝑥
6 4 5 eqtr4i ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥 , 𝑦
7 fveq2 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st𝐴 ) = ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8 inteq ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐴 = 𝑥 , 𝑦 ⟩ )
9 8 inteqd ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐴 = 𝑥 , 𝑦 ⟩ )
10 6 7 9 3eqtr4a ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st𝐴 ) = 𝐴 )
11 10 exlimivv ( ∃ 𝑥𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st𝐴 ) = 𝐴 )
12 1 11 sylbi ( 𝐴 ∈ ( V × V ) → ( 1st𝐴 ) = 𝐴 )