Theorem cnvepresdmqss

Description: The domain quotient binary relation of the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021)

	Ref	Expression
Assertion	cnvepresdmqss	$$⊢A\in V\to \left(\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{DomainQss}A\leftrightarrow \neg \varnothing \in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnvepresex	$$⊢A\in V\to {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{V}$$
2		brdmqss	$$⊢\left(A\in V\wedge {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{V}\right)\to \left(\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{DomainQss}A\leftrightarrow \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)$$
3	1 2	mpdan	$$⊢A\in V\to \left(\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{DomainQss}A\leftrightarrow \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)$$
4		n0el3	$$⊢\neg \varnothing \in A\leftrightarrow \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$
5	3 4	bitr4di	$$⊢A\in V\to \left(\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{DomainQss}A\leftrightarrow \neg \varnothing \in A\right)$$