Theorem fv2prop

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	fv2prop	⊢ ( 𝐵 ∈ 𝑉 → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 2 ) = 𝐵 )

Proof

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