Metamath Proof Explorer


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 -1 A Part A E -1 A ErALTV A

Proof

Step Hyp Ref Expression
1 mpet MembPart A CoMembEr A
2 df-membpart MembPart A E -1 A Part A
3 df-comember CoMembEr A E -1 A ErALTV A
4 1 2 3 3bitr3i E -1 A Part A E -1 A ErALTV A