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		vex	⊢ 𝑥 ∈ V
2		eldif	⊢ ( 𝑥 ∈ ( V ∖ 𝐵 ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐵 ) )
3	1 2	mpbiran	⊢ ( 𝑥 ∈ ( V ∖ 𝐵 ) ↔ ¬ 𝑥 ∈ 𝐵 )
4	3	con2bii	⊢ ( 𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ ( V ∖ 𝐵 ) )
5	4	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( V ∖ 𝐵 ) ) )
6		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( V ∖ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( V ∖ 𝐵 ) ) )
7	5 6	bitr4i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ( 𝐴 ∖ ( V ∖ 𝐵 ) ) )
8	7	ineqri	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∖ ( V ∖ 𝐵 ) )