Theorem dfin2 4223

Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4222. Another version is given by dfin4 4230. (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		velcomp 3919	. . . . 5 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ ¬ 𝑥 ∈ 𝐵)
2	1	con2bii 360	. . . 4 ⊢ (𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ (V ∖ 𝐵))
3	2	anbi2i 634	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
4		eldif 3914	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
5	3, 4	bitr4i 281	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)))
6	5	ineqri 4164	1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵))

Syntax hints:  ¬ wn 3   ∧ wa 400   = wceq 1568   ∈ wcel 2141  Vcvv 3453   ∖ cdif 3901   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3907  df-in 3911

This theorem is referenced by:  dfun3  4228  dfin3  4229  invdif  4231  difundi  4242  difindi  4244  difdif2  4248