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	eqtrdi	$⊢ \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 x) \to A \in V$
8	7	stoic1a	$⊢ (Rel R \land \neg A \in V) \to \neg A R x$
9	8	alrimiv	$⊢ (Rel R \land \neg A \in V) \to \forall x \neg A R x$
10		breq2	$⊢ y = x \to (A R y \leftrightarrow A R x)$
11	10	ab0w	$⊢ \{y \| A R y\} = \emptyset \leftrightarrow \forall x \neg A R x$
12	9 11	sylibr	$⊢ (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