Theorem fv1prop

Description: The function value of unordered pair of ordered pairs with first components 1 and 2 at 1. (Contributed by AV, 4-Feb-2023)

	Ref	Expression
Assertion	fv1prop	⊢ ( 𝐴 ∈ 𝑉 → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		1ex	⊢ 1 ∈ V
2		1ne2	⊢ 1 ≠ 2
3		fvpr1g	⊢ ( ( 1 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 )
4	1 2 3	mp3an13	⊢ ( 𝐴 ∈ 𝑉 → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 )