Theorem brparts

Description: Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021)

	Ref	Expression
Assertion	brparts	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑅 Parts 𝐴 ↔ ( 𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-parts	⊢ Parts = ( DomainQss ↾ Disjs )
2	1	eqres	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑅 Parts 𝐴 ↔ ( 𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴 ) ) )