Theorem dfin2 4234

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

Assertion

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

Proof of Theorem dfin2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3451	. . . . . 6 ⊢ 𝑥 ∈ V
2		eldif 3924	. . . . . 6 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	mpbiran 709	. . . . 5 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ ¬ 𝑥 ∈ 𝐵)
4	3	con2bii 357	. . . 4 ⊢ (𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ (V ∖ 𝐵))
5	4	anbi2i 623	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
6		eldif 3924	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
7	5, 6	bitr4i 278	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)))
8	7	ineqri 4175	1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵))

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ∖ cdif 3911   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-in 3921

This theorem is referenced by:  dfun3  4239  dfin3  4240  invdif  4242  difundi  4253  difindi  4255  difdif2  4259