dmcnvep

Description: Domain of converse epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018) (Revised by Peter Mazsa, 23-Nov-2025)

		Ref	Expression
	Assertion	dmcnvep	$⊢ dom E^{-1} = V ∖ \{\emptyset\}$

Step	Hyp	Ref	Expression
1		df-dm	$⊢ dom E^{-1} = \{x \| \exists y x E^{-1} y\}$
2		brcnvep	$⊢ x \in V \to (x E^{-1} y \leftrightarrow y \in x)$
3	2	elv	$⊢ x E^{-1} y \leftrightarrow y \in x$
4	3	exbii	$⊢ \exists y x E^{-1} y \leftrightarrow \exists y y \in x$
5	4	abbii	$⊢ \{x \| \exists y x E^{-1} y\} = \{x \| \exists y y \in x\}$
6		df-sn	$⊢ \{\emptyset\} = \{x \| x = \emptyset\}$
7	6	difeq2i	$⊢ V ∖ \{\emptyset\} = V ∖ \{x \| x = \emptyset\}$
8		notab	$⊢ \{x \| \neg x = \emptyset\} = V ∖ \{x \| x = \emptyset\}$
9		neq0	$⊢ \neg x = \emptyset \leftrightarrow \exists y y \in x$
10	9	abbii	$⊢ \{x \| \neg x = \emptyset\} = \{x \| \exists y y \in x\}$
11	7 8 10	3eqtr2ri	$⊢ \{x \| \exists y y \in x\} = V ∖ \{\emptyset\}$
12	1 5 11	3eqtri	$⊢ dom E^{-1} = V ∖ \{\emptyset\}$

Metamath Proof Explorer