imasng

		Ref	Expression
	Assertion	imasng	$⊢ A \in B \to R [\{A\}] = \{y \| A R y\}$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in B \to A \in V$
2		dfima2	$⊢ R [\{A\}] = \{y \| \exists x \in \{A\} x R y\}$
3		breq1	$⊢ x = A \to (x R y \leftrightarrow A R y)$
4	3	rexsng	$⊢ A \in V \to (\exists x \in \{A\} x R y \leftrightarrow A R y)$
5	4	abbidv	$⊢ A \in V \to \{y \| \exists x \in \{A\} x R y\} = \{y \| A R y\}$
6	2 5	eqtrid	$⊢ A \in V \to R [\{A\}] = \{y \| A R y\}$
7	1 6	syl	$⊢ A \in B \to R [\{A\}] = \{y \| A R y\}$

Metamath Proof Explorer