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

Metamath Proof Explorer

Theorem s1rn

Description: The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016)

		Ref	Expression
	Assertion	s1rn	$⊢ A \in V \to ran ⟨“ A ”⟩ = \{A\}$

Step	Hyp	Ref	Expression
1		s1val	$⊢ A \in V \to ⟨“ A ”⟩ = \{⟨0, A⟩\}$
2	1	rneqd	$⊢ A \in V \to ran ⟨“ A ”⟩ = ran \{⟨0, A⟩\}$
3		c0ex	$⊢ 0 \in V$
4	3	rnsnop	$⊢ ran \{⟨0, A⟩\} = \{A\}$
5	2 4	eqtrdi	$⊢ A \in V \to ran ⟨“ A ”⟩ = \{A\}$