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

Metamath Proof Explorer

Theorem s1prc

Description: Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022)

		Ref	Expression
	Assertion	s1prc	$⊢ \neg A \in V \to ⟨“ A ”⟩ = ⟨“ \emptyset ”⟩$

Step	Hyp	Ref	Expression
1		ids1	$⊢ ⟨“ A ”⟩ = ⟨“ I (A) ”⟩$
2		fvprc	$⊢ \neg A \in V \to I (A) = \emptyset$
3	2	s1eqd	$⊢ \neg A \in V \to ⟨“ I (A) ”⟩ = ⟨“ \emptyset ”⟩$
4	1 3	eqtrid	$⊢ \neg A \in V \to ⟨“ A ”⟩ = ⟨“ \emptyset ”⟩$