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 , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )