Theorem dfpart2

Description: Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021)

	Ref	Expression
Assertion	dfpart2	Could not format assertion : No typesetting found for |- ( R Part A <-> ( Disj R /\ ( dom R /. R ) = A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-part	Could not format ( R Part A <-> ( Disj R /\ R DomainQs A ) ) : No typesetting found for |- ( R Part A <-> ( Disj R /\ R DomainQs A ) ) with typecode |-
2		df-dmqs	$$⊢RDomainQsA\leftrightarrow \mathrm{dom}R/R=A$$
3	2	anbi2i	$$⊢\left(DisjR\wedge RDomainQsA\right)\leftrightarrow \left(DisjR\wedge \mathrm{dom}R/R=A\right)$$
4	1 3	bitri	Could not format ( R Part A <-> ( Disj R /\ ( dom R /. R ) = A ) ) : No typesetting found for |- ( R Part A <-> ( Disj R /\ ( dom R /. R ) = A ) ) with typecode |-