Theorem dfin2

Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 . Another version is given by dfin4 . (Contributed by NM, 10-Jun-2004)

	Ref	Expression
Assertion	dfin2	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∖ ( V ∖ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		velcomp	⊢ ( 𝑥 ∈ ( V ∖ 𝐵 ) ↔ ¬ 𝑥 ∈ 𝐵 )
2	1	con2bii	⊢ ( 𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ ( V ∖ 𝐵 ) )
3	2	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( V ∖ 𝐵 ) ) )
4		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( V ∖ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( V ∖ 𝐵 ) ) )
5	3 4	bitr4i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ( 𝐴 ∖ ( V ∖ 𝐵 ) ) )
6	5	ineqri	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∖ ( V ∖ 𝐵 ) )