Metamath Proof Explorer

Theorem suppvalbr

Description: The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019) (Proof shortened by Sky Winter, 14-Oct-2026)

		Ref	Expression
	Assertion	suppvalbr	$⊢ (R \in V \land Z \in W) \to R supp Z = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$

Proof

Step	Hyp	Ref	Expression
1		suppval	$⊢ (R \in V \land Z \in W) \to R supp Z = \{x \in dom R \| R [\{x\}] \neq \{Z\}\}$
2		df-rab	$⊢ \{x \in dom R \| R [\{x\}] \neq \{Z\}\} = \{x \| (x \in dom R \land R [\{x\}] \neq \{Z\})\}$
3		vex	$⊢ x \in V$
4	3	eldm	$⊢ x \in dom R \leftrightarrow \exists y x R y$
5		nabbib	$⊢ \{y \| x R y\} \neq \{y \| y = Z\} \leftrightarrow \exists y (x R y \leftrightarrow \neg y = Z)$
6		imasng	$⊢ x \in V \to R [\{x\}] = \{y \| x R y\}$
7	6	elv	$⊢ R [\{x\}] = \{y \| x R y\}$
8		df-sn	$⊢ \{Z\} = \{y \| y = Z\}$
9	7 8	neeq12i	$⊢ R [\{x\}] \neq \{Z\} \leftrightarrow \{y \| x R y\} \neq \{y \| y = Z\}$
10		df-ne	$⊢ y \neq Z \leftrightarrow \neg y = Z$
11	10	bibi2i	$⊢ (x R y \leftrightarrow y \neq Z) \leftrightarrow (x R y \leftrightarrow \neg y = Z)$
12	11	exbii	$⊢ \exists y (x R y \leftrightarrow y \neq Z) \leftrightarrow \exists y (x R y \leftrightarrow \neg y = Z)$
13	5 9 12	3bitr4i	$⊢ R [\{x\}] \neq \{Z\} \leftrightarrow \exists y (x R y \leftrightarrow y \neq Z)$
14	4 13	anbi12i	$⊢ (x \in dom R \land R [\{x\}] \neq \{Z\}) \leftrightarrow (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))$
15	14	abbii	$⊢ \{x \| (x \in dom R \land R [\{x\}] \neq \{Z\})\} = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$
16	2 15	eqtri	$⊢ \{x \in dom R \| R [\{x\}] \neq \{Z\}\} = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$
17	1 16	eqtrdi	$⊢ (R \in V \land Z \in W) \to R supp Z = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$