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	⊢ ( ¬ 𝐴 ∈ V → ⟨“ 𝐴 ”⟩ = ⟨“ ∅ ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		ids1	⊢ ⟨“ 𝐴 ”⟩ = ⟨“ ( I ‘ 𝐴 ) ”⟩
2		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( I ‘ 𝐴 ) = ∅ )
3	2	s1eqd	⊢ ( ¬ 𝐴 ∈ V → ⟨“ ( I ‘ 𝐴 ) ”⟩ = ⟨“ ∅ ”⟩ )
4	1 3	eqtrid	⊢ ( ¬ 𝐴 ∈ V → ⟨“ 𝐴 ”⟩ = ⟨“ ∅ ”⟩ )