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

Proof

Step	Hyp	Ref	Expression
1		mpet	Could not format ( MembPart A <-> CoMembEr A ) : No typesetting found for |- ( MembPart A <-> CoMembEr A ) with typecode |-
2		df-membpart	Could not format ( MembPart A <-> ( `' _E |` A ) Part A ) : No typesetting found for |- ( MembPart A <-> ( `' _E |` A ) Part A ) with typecode |-
3		df-comember	Could not format ( CoMembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) : No typesetting found for |- ( CoMembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) with typecode |-
4	1 2 3	3bitr3i	Could not format ( ( `' _E |` A ) Part A <-> ,~ ( `' _E |` A ) ErALTV A ) : No typesetting found for |- ( ( `' _E |` A ) Part A <-> ,~ ( `' _E |` A ) ErALTV A ) with typecode |-