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

Proof

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