Theorem difres

Description: Case when class difference in unaffected by restriction. (Contributed by Thierry Arnoux, 1-Jan-2020)

	Ref	Expression
Assertion	difres	|- ( A C_ ( B X. _V ) -> ( A \ ( C |` B ) ) = ( A \ C ) )

Proof

Step	Hyp	Ref	Expression
1		df-res	|- ( C |` B ) = ( C i^i ( B X. _V ) )
2	1	difeq2i	|- ( A \ ( C |` B ) ) = ( A \ ( C i^i ( B X. _V ) ) )
3		difindi	|- ( A \ ( C i^i ( B X. _V ) ) ) = ( ( A \ C ) u. ( A \ ( B X. _V ) ) )
4		ssdif	|- ( A C_ ( B X. _V ) -> ( A \ ( B X. _V ) ) C_ ( ( B X. _V ) \ ( B X. _V ) ) )
5		difid	|- ( ( B X. _V ) \ ( B X. _V ) ) = (/)
6	4 5	sseqtrdi	|- ( A C_ ( B X. _V ) -> ( A \ ( B X. _V ) ) C_ (/) )
7		ss0	|- ( ( A \ ( B X. _V ) ) C_ (/) -> ( A \ ( B X. _V ) ) = (/) )
8	6 7	syl	|- ( A C_ ( B X. _V ) -> ( A \ ( B X. _V ) ) = (/) )
9	8	uneq2d	|- ( A C_ ( B X. _V ) -> ( ( A \ C ) u. ( A \ ( B X. _V ) ) ) = ( ( A \ C ) u. (/) ) )
10	3 9	syl5eq	|- ( A C_ ( B X. _V ) -> ( A \ ( C i^i ( B X. _V ) ) ) = ( ( A \ C ) u. (/) ) )
11		un0	|- ( ( A \ C ) u. (/) ) = ( A \ C )
12	10 11	eqtrdi	|- ( A C_ ( B X. _V ) -> ( A \ ( C i^i ( B X. _V ) ) ) = ( A \ C ) )
13	2 12	syl5eq	|- ( A C_ ( B X. _V ) -> ( A \ ( C |` B ) ) = ( A \ C ) )