This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmcnvepres

Description: Domain of the restricted converse epsilon relation. (Contributed by Peter Mazsa, 28-Jan-2026)

		Ref	Expression
	Assertion	dmcnvepres	$⊢ dom ({E^{-1} ↾}_{A}) = A ∖ \{\emptyset\}$

Step	Hyp	Ref	Expression
1		dmres	$⊢ dom ({E^{-1} ↾}_{A}) = A \cap dom E^{-1}$
2		dmcnvep	$⊢ dom E^{-1} = V ∖ \{\emptyset\}$
3	2	ineq2i	$⊢ A \cap dom E^{-1} = A \cap (V ∖ \{\emptyset\})$
4		invdif	$⊢ A \cap (V ∖ \{\emptyset\}) = A ∖ \{\emptyset\}$
5	1 3 4	3eqtri	$⊢ dom ({E^{-1} ↾}_{A}) = A ∖ \{\emptyset\}$