This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} (\emptyset) = A$

Step	Hyp	Ref	Expression
1		peano1	$⊢ \emptyset \in ω$
2		1n0	$⊢ 1_{𝑜} \neq \emptyset$
3	2	necomi	$⊢ \emptyset \neq 1_{𝑜}$
4		fvpr1g	$⊢ (\emptyset \in ω \land A \in V \land \emptyset \neq 1_{𝑜}) \to \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} (\emptyset) = A$
5	1 3 4	mp3an13	$⊢ A \in V \to \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} (\emptyset) = A$