Metamath Proof Explorer


Theorem brpartspart

Description: Binary partition and the partition predicate are the same if A and R are sets. (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion brpartspart A V R W R Parts A R Part A

Proof

Step Hyp Ref Expression
1 eldisjsdisj R W R Disjs Disj R
2 1 adantl A V R W R Disjs Disj R
3 brdmqssqs A V R W R DomainQss A R DomainQs A
4 2 3 anbi12d A V R W R Disjs R DomainQss A Disj R R DomainQs A
5 brparts A V R Parts A R Disjs R DomainQss A
6 5 adantr A V R W R Parts A R Disjs R DomainQss A
7 df-part R Part A Disj R R DomainQs A
8 7 a1i A V R W R Part A Disj R R DomainQs A
9 4 6 8 3bitr4d A V R W R Parts A R Part A