Theorem fvpr1o

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

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

Proof

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