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	$$⊢A\in V\to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(\varnothing \right)=A$$

Proof

Step	Hyp	Ref	Expression
1		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
2		1n0	$$⊢1_{𝑜}\ne \varnothing$$
3	2	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
4		fvpr1g	$$⊢\left(\varnothing \in \mathrm{\omega }\wedge A\in V\wedge \varnothing \ne 1_{𝑜}\right)\to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(\varnothing \right)=A$$
5	1 3 4	mp3an13	$$⊢A\in V\to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(\varnothing \right)=A$$