Theorem fvpr1

Description: The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010)

	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		df-pr	⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
4	3	fveq1i	⊢ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = ( ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ‘ 𝐴 )
5		necom	⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
6		fvunsn	⊢ ( 𝐵 ≠ 𝐴 → ( ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) )
7	5 6	sylbi	⊢ ( 𝐴 ≠ 𝐵 → ( ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) )
8	4 7	eqtrid	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) )
9	1 2	fvsn	⊢ ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) = 𝐶
10	8 9	eqtrdi	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = 𝐶 )