relimasn

		Ref	Expression
	Assertion	relimasn	$⊢ Rel R \to R [\{A\}] = \{y \| A R y\}$

Step	Hyp	Ref	Expression
1		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
2		imaeq2	$⊢ \{A\} = \emptyset \to R [\{A\}] = R [\emptyset]$
3	1 2	sylbi	$⊢ \neg A \in V \to R [\{A\}] = R [\emptyset]$
4		ima0	$⊢ R [\emptyset] = \emptyset$
5	3 4	syl6eq	$⊢ \neg A \in V \to R [\{A\}] = \emptyset$
6	5	adantl	$⊢ (Rel R \land \neg A \in V) \to R [\{A\}] = \emptyset$
7		brrelex1	$⊢ (Rel R \land A R y) \to A \in V$
8	7	stoic1a	$⊢ (Rel R \land \neg A \in V) \to \neg A R y$
9	8	nexdv	$⊢ (Rel R \land \neg A \in V) \to \neg \exists y A R y$
10		abn0	$⊢ \{y \| A R y\} \neq \emptyset \leftrightarrow \exists y A R y$
11	10	necon1bbii	$⊢ \neg \exists y A R y \leftrightarrow \{y \| A R y\} = \emptyset$
12	9 11	sylib	$⊢ (Rel R \land \neg A \in V) \to \{y \| A R y\} = \emptyset$
13	6 12	eqtr4d	$⊢ (Rel R \land \neg A \in V) \to R [\{A\}] = \{y \| A R y\}$
14	13	ex	$⊢ Rel R \to (\neg A \in V \to R [\{A\}] = \{y \| A R y\})$
15		imasng	$⊢ A \in V \to R [\{A\}] = \{y \| A R y\}$
16	14 15	pm2.61d2	$⊢ Rel R \to R [\{A\}] = \{y \| A R y\}$

Metamath Proof Explorer