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 \mathrm{V}\to ⟨“A”⟩=⟨“\varnothing ”⟩$$

Proof

Step	Hyp	Ref	Expression
1		ids1	$$⊢⟨“A”⟩=⟨“\mathrm{I}\left(A\right)”⟩$$
2		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{I}\left(A\right)=\varnothing$$
3	2	s1eqd	$$⊢\neg A\in \mathrm{V}\to ⟨“\mathrm{I}\left(A\right)”⟩=⟨“\varnothing ”⟩$$
4	1 3	syl5eq	$$⊢\neg A\in \mathrm{V}\to ⟨“A”⟩=⟨“\varnothing ”⟩$$