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	Could not format assertion : No typesetting found for |- ( (/) Part A <-> ,~ (/) ErALTV A ) with typecode |-

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	Could not format ( (/) Part A <-> ( Disj (/) /\ ( dom (/) /. (/) ) = A ) ) : No typesetting found for |- ( (/) Part A <-> ( Disj (/) /\ ( dom (/) /. (/) ) = A ) ) with typecode |-
3		dferALTV2	$$⊢\wr \varnothing ErALTVA\leftrightarrow \left(EqvRel\wr \varnothing \wedge \mathrm{dom}\wr \varnothing /\wr \varnothing =A\right)$$
4	1 2 3	3bitr4i	Could not format ( (/) Part A <-> ,~ (/) ErALTV A ) : No typesetting found for |- ( (/) Part A <-> ,~ (/) ErALTV A ) with typecode |-