This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem parteq1

Description: Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021)

		Ref	Expression
	Assertion	parteq1	$⊢ R = S \to (R Part A \leftrightarrow S Part A)$

Step	Hyp	Ref	Expression
1		disjdmqseqeq1	$⊢ R = S \to ((Disj R \land dom R / R = A) \leftrightarrow (Disj S \land dom S / S = A))$
2		dfpart2	$⊢ R Part A \leftrightarrow (Disj R \land dom R / R = A)$
3		dfpart2	$⊢ S Part A \leftrightarrow (Disj S \land dom S / S = A)$
4	1 2 3	3bitr4g	$⊢ R = S \to (R Part A \leftrightarrow S Part A)$