This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvpr1g

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 fvpr1g ⊢ A ∈ V ∧ C ∈ W ∧ A ≠ B → A C B D ⁡ A = C

Proof

Step Hyp Ref Expression
1 df-pr ⊢ A C B D = A C ∪ B D
2 1 fveq1i ⊢ A C B D ⁡ A = A C ∪ B D ⁡ A
3 necom ⊢ A ≠ B ↔ B ≠ A
4 fvunsn ⊢ B ≠ A → A C ∪ B D ⁡ A = A C ⁡ A
5 3 4 sylbi ⊢ A ≠ B → A C ∪ B D ⁡ A = A C ⁡ A
6 2 5 eqtrid ⊢ A ≠ B → A C B D ⁡ A = A C ⁡ A
7 6 3ad2ant3 ⊢ A ∈ V ∧ C ∈ W ∧ A ≠ B → A C B D ⁡ A = A C ⁡ A
8 fvsng ⊢ A ∈ V ∧ C ∈ W → A C ⁡ A = C
9 8 3adant3 ⊢ A ∈ V ∧ C ∈ W ∧ A ≠ B → A C ⁡ A = C
10 7 9 eqtrd ⊢ A ∈ V ∧ C ∈ W ∧ A ≠ B → A C B D ⁡ A = C