Theorem mpet2

Description: Member Partition-Equivalence Theorem in a shorter form. Together with mpet mpet3 , mostly in its conventional cpet and cpet2 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 with general R ). (Contributed by Peter Mazsa, 24-Sep-2021)

	Ref	Expression
Assertion	mpet2	|- ( ( `' _E |` A ) Part A <-> ,~ ( `' _E |` A ) ErALTV A )

Proof

Step	Hyp	Ref	Expression
1		mpet	|- ( MembPart A <-> CoMembEr A )
2		df-membpart	|- ( MembPart A <-> ( `' _E |` A ) Part A )
3		df-comember	|- ( CoMembEr A <-> ,~ ( `' _E |` A ) ErALTV A )
4	1 2 3	3bitr3i	|- ( ( `' _E |` A ) Part A <-> ,~ ( `' _E |` A ) ErALTV A )