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