Metamath Proof Explorer

Theorem petincnvepres2

Description: A partition-equivalence theorem with intersection and general R . (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion petincnvepres2 ⊢DisjR∩E-1↾A∧dom⁡R∩E-1↾A/R∩E-1↾A=A↔EqvRel≀R∩E-1↾A∧dom⁡≀R∩E-1↾A/≀R∩E-1↾A=A

Proof

Step Hyp Ref Expression
1 eqvrelqseqdisj4 ⊢EqvRel≀R∩E-1↾A∧dom⁡≀R∩E-1↾A/≀R∩E-1↾A=A→DisjR∩E-1↾A
2 1 petlem ⊢DisjR∩E-1↾A∧dom⁡R∩E-1↾A/R∩E-1↾A=A↔EqvRel≀R∩E-1↾A∧dom⁡≀R∩E-1↾A/≀R∩E-1↾A=A