Theorem difres

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

	Ref	Expression
Assertion	difres	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → ( 𝐴 ∖ ( 𝐶 ↾ 𝐵 ) ) = ( 𝐴 ∖ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		df-res	⊢ ( 𝐶 ↾ 𝐵 ) = ( 𝐶 ∩ ( 𝐵 × V ) )
2	1	difeq2i	⊢ ( 𝐴 ∖ ( 𝐶 ↾ 𝐵 ) ) = ( 𝐴 ∖ ( 𝐶 ∩ ( 𝐵 × V ) ) )
3		difindi	⊢ ( 𝐴 ∖ ( 𝐶 ∩ ( 𝐵 × V ) ) ) = ( ( 𝐴 ∖ 𝐶 ) ∪ ( 𝐴 ∖ ( 𝐵 × V ) ) )
4		ssdif	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → ( 𝐴 ∖ ( 𝐵 × V ) ) ⊆ ( ( 𝐵 × V ) ∖ ( 𝐵 × V ) ) )
5		difid	⊢ ( ( 𝐵 × V ) ∖ ( 𝐵 × V ) ) = ∅
6	4 5	sseqtrdi	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → ( 𝐴 ∖ ( 𝐵 × V ) ) ⊆ ∅ )
7		ss0	⊢ ( ( 𝐴 ∖ ( 𝐵 × V ) ) ⊆ ∅ → ( 𝐴 ∖ ( 𝐵 × V ) ) = ∅ )
8	6 7	syl	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → ( 𝐴 ∖ ( 𝐵 × V ) ) = ∅ )
9	8	uneq2d	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → ( ( 𝐴 ∖ 𝐶 ) ∪ ( 𝐴 ∖ ( 𝐵 × V ) ) ) = ( ( 𝐴 ∖ 𝐶 ) ∪ ∅ ) )
10	3 9	syl5eq	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → ( 𝐴 ∖ ( 𝐶 ∩ ( 𝐵 × V ) ) ) = ( ( 𝐴 ∖ 𝐶 ) ∪ ∅ ) )
11		un0	⊢ ( ( 𝐴 ∖ 𝐶 ) ∪ ∅ ) = ( 𝐴 ∖ 𝐶 )
12	10 11	eqtrdi	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → ( 𝐴 ∖ ( 𝐶 ∩ ( 𝐵 × V ) ) ) = ( 𝐴 ∖ 𝐶 ) )
13	2 12	syl5eq	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → ( 𝐴 ∖ ( 𝐶 ↾ 𝐵 ) ) = ( 𝐴 ∖ 𝐶 ) )