Metamath Proof Explorer

Theorem disjresdif

Description: The difference between restrictions to disjoint is the first restriction. (Contributed by Peter Mazsa, 24-Jul-2024)

		Ref	Expression
	Assertion	disjresdif	\|- ( ( A i^i B ) = (/) -> ( ( R \|` A ) \ ( R \|` B ) ) = ( R \|` A ) )

Step	Hyp	Ref	Expression
1		disjresdisj	\|- ( ( A i^i B ) = (/) -> ( ( R \|` A ) i^i ( R \|` B ) ) = (/) )
2		disjdif2	\|- ( ( ( R \|` A ) i^i ( R \|` B ) ) = (/) -> ( ( R \|` A ) \ ( R \|` B ) ) = ( R \|` A ) )
3	1 2	syl	\|- ( ( A i^i B ) = (/) -> ( ( R \|` A ) \ ( R \|` B ) ) = ( R \|` A ) )

Step

Hyp

Ref

Expression

 |-  ( ( A i^i B ) = (/) -> ( ( R |` A ) i^i ( R |` B ) ) = (/) )

 |-  ( ( ( R |` A ) i^i ( R |` B ) ) = (/) -> ( ( R |` A ) \ ( R |` B ) ) = ( R |` A ) )

1 2

 |-  ( ( A i^i B ) = (/) -> ( ( R |` A ) \ ( R |` B ) ) = ( R |` A ) )