Metamath Proof Explorer

Theorem mainpart

Description: Partition with general R also imply member partition. (Contributed by Peter Mazsa, 23-Sep-2021) (Revised by Peter Mazsa, 22-Dec-2024)

Ref Expression
Assertion mainpart 
|- ( R Part A -> MembPart A )

Proof

Step Hyp Ref Expression
1 partimcomember 
 |-  ( R Part A -> CoMembEr A )
2 mpet 
 |-  ( MembPart A <-> CoMembEr A )
3 1 2 sylibr 
 |-  ( R Part A -> MembPart A )