Theorem eldisjn0elb

Description: Two forms of disjoint elements when the empty set is not an element of the class. (Contributed by Peter Mazsa, 31-Dec-2024)

	Ref	Expression
Assertion	eldisjn0elb	$$⊢\left(ElDisjA\wedge \neg \varnothing \in A\right)\leftrightarrow \left(Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-eldisj	$$⊢ElDisjA\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
2		n0el3	$$⊢\neg \varnothing \in A\leftrightarrow \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$
3	1 2	anbi12i	$$⊢\left(ElDisjA\wedge \neg \varnothing \in A\right)\leftrightarrow \left(Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)$$