Metamath Proof Explorer


Theorem fvpr2

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

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

Proof

Step Hyp Ref Expression
1 fvpr2.1 𝐵 ∈ V
2 fvpr2.2 𝐷 ∈ V
3 prcom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ }
4 3 fveq1i ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = ( { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐵 )
5 necom ( 𝐴𝐵𝐵𝐴 )
6 1 2 fvpr1 ( 𝐵𝐴 → ( { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐵 ) = 𝐷 )
7 5 6 sylbi ( 𝐴𝐵 → ( { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐵 ) = 𝐷 )
8 4 7 eqtrid ( 𝐴𝐵 → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = 𝐷 )