Theorem pet0

Description: Class A is a partition by the null class if and only if the cosets by the null class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021)

	Ref	Expression
Assertion	pet0	$$⊢\varnothing PartA\leftrightarrow \wr \varnothing ErALTVA$$

Proof

Step	Hyp	Ref	Expression
1		pet02	$$⊢\left(Disj\varnothing \wedge \mathrm{dom}\varnothing /\varnothing =A\right)\leftrightarrow \left(EqvRel\wr \varnothing \wedge \mathrm{dom}\wr \varnothing /\wr \varnothing =A\right)$$
2		dfpart2	$$⊢\varnothing PartA\leftrightarrow \left(Disj\varnothing \wedge \mathrm{dom}\varnothing /\varnothing =A\right)$$
3		dferALTV2	$$⊢\wr \varnothing ErALTVA\leftrightarrow \left(EqvRel\wr \varnothing \wedge \mathrm{dom}\wr \varnothing /\wr \varnothing =A\right)$$
4	1 2 3	3bitr4i	$$⊢\varnothing PartA\leftrightarrow \wr \varnothing ErALTVA$$