Theorem dfin2 4059

Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4058. Another version is given by dfin4 4066. (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 3386	. . . . . 6 ⊢ 𝑥 ∈ V
2		eldif 3777	. . . . . 6 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	mpbiran 701	. . . . 5 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ ¬ 𝑥 ∈ 𝐵)
4	3	con2bii 349	. . . 4 ⊢ (𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ (V ∖ 𝐵))
5	4	anbi2i 617	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
6		eldif 3777	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
7	5, 6	bitr4i 270	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)))
8	7	ineqri 4002	1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵))

Syntax hints:  ¬ wn 3   ∧ wa 385   = wceq 1653   ∈ wcel 2157  Vcvv 3383   ∖ cdif 3764   ∩ cin 3766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-v 3385  df-dif 3770  df-in 3774

This theorem is referenced by:  dfun3  4064  dfin3  4065  invdif  4067  difundi  4078  difindi  4080  difdif2  4083