Theorem parteq12

Description: Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024)

	Ref	Expression
Assertion	parteq12	Could not format assertion : No typesetting found for |- ( ( R = S /\ A = B ) -> ( R Part A <-> S Part B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		parteq1	Could not format ( R = S -> ( R Part A <-> S Part A ) ) : No typesetting found for |- ( R = S -> ( R Part A <-> S Part A ) ) with typecode |-
2		parteq2	Could not format ( A = B -> ( S Part A <-> S Part B ) ) : No typesetting found for |- ( A = B -> ( S Part A <-> S Part B ) ) with typecode |-
3	1 2	sylan9bb	Could not format ( ( R = S /\ A = B ) -> ( R Part A <-> S Part B ) ) : No typesetting found for |- ( ( R = S /\ A = B ) -> ( R Part A <-> S Part B ) ) with typecode |-