Theorem fvpr1

Description: The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010) (Proof shortened by BJ, 26-Sep-2024)

	Ref	Expression
Hypotheses	fvpr1.1	⊢ 𝐴 ∈ V
	fvpr1.2	⊢ 𝐶 ∈ V
Assertion	fvpr1	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvpr1.1	⊢ 𝐴 ∈ V
2		fvpr1.2	⊢ 𝐶 ∈ V
3		fvpr1g	⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = 𝐶 )
4	1 2 3	mp3an12	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = 𝐶 )