Theorem fvpr2g

Description: The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017)

	Ref	Expression
Assertion	fvpr2g	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		prcom	⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ }
2		df-pr	⊢ { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } = ( { ⟨ 𝐵 , 𝐷 ⟩ } ∪ { ⟨ 𝐴 , 𝐶 ⟩ } )
3	1 2	eqtri	⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐵 , 𝐷 ⟩ } ∪ { ⟨ 𝐴 , 𝐶 ⟩ } )
4	3	fveq1i	⊢ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = ( ( { ⟨ 𝐵 , 𝐷 ⟩ } ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ‘ 𝐵 )
5		fvunsn	⊢ ( 𝐴 ≠ 𝐵 → ( ( { ⟨ 𝐵 , 𝐷 ⟩ } ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ‘ 𝐵 ) = ( { ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) )
6	4 5	syl5eq	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = ( { ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) )
7	6	3ad2ant3	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = ( { ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) )
8		fvsng	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ( { ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = 𝐷 )
9	8	3adant3	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = 𝐷 )
10	7 9	eqtrd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = 𝐷 )