Theorem dfin4

Description: Alternate definition of the intersection of two classes. Exercise 4.10(q) of Mendelson p. 231. (Contributed by NM, 25-Nov-2003)

	Ref	Expression
Assertion	dfin4	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
2		dfss4	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) ) = ( 𝐴 ∩ 𝐵 ) )
3	1 2	mpbi	⊢ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) ) = ( 𝐴 ∩ 𝐵 )
4		difin	⊢ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
5	4	difeq2i	⊢ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) )
6	3 5	eqtr3i	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) )