Metamath Proof Explorer


Theorem fvpr0o

Description: The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023)

Ref Expression
Assertion fvpr0o ( 𝐴𝑉 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 peano1 ∅ ∈ ω
2 1n0 1o ≠ ∅
3 2 necomi ∅ ≠ 1o
4 fvpr1g ( ( ∅ ∈ ω ∧ 𝐴𝑉 ∧ ∅ ≠ 1o ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
5 1 3 4 mp3an13 ( 𝐴𝑉 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )