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 , 𝐵 〉 } ‘ ∅ ) = 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | peano1 | ⊢ ∅ ∈ ω | |
2 | 1n0 | ⊢ 1o ≠ ∅ | |
3 | 2 | necomi | ⊢ ∅ ≠ 1o |
4 | fvpr1g | ⊢ ( ( ∅ ∈ ω ∧ 𝐴 ∈ 𝑉 ∧ ∅ ≠ 1o ) → ( { 〈 ∅ , 𝐴 〉 , 〈 1o , 𝐵 〉 } ‘ ∅ ) = 𝐴 ) | |
5 | 1 3 4 | mp3an13 | ⊢ ( 𝐴 ∈ 𝑉 → ( { 〈 ∅ , 𝐴 〉 , 〈 1o , 𝐵 〉 } ‘ ∅ ) = 𝐴 ) |