Theorem dfun2 4221

Description: An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4222 and dfss4 4220 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation ∖ (class difference). (Contributed by NM, 10-Jun-2004.)

Assertion

Ref	Expression
dfun2	⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∖ 𝐵))

Proof of Theorem dfun2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3440	. . . . . . 7 ⊢ 𝑥 ∈ V
2		eldif 3913	. . . . . . 7 ⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐴))
3	1, 2	mpbiran 709	. . . . . 6 ⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴)
4	3	anbi1i 624	. . . . 5 ⊢ ((𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
5		eldif 3913	. . . . 5 ⊢ (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ (𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥 ∈ 𝐵))
6		ioran 985	. . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
7	4, 5, 6	3bitr4i 303	. . . 4 ⊢ (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
8	7	con2bii 357	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵))
9		eldif 3913	. . . 4 ⊢ (𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵)))
10	1, 9	mpbiran 709	. . 3 ⊢ (𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) ↔ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵))
11	8, 10	bitr4i 278	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)))
12	11	uneqri 4107	1 ⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∖ 𝐵))

Syntax hints:  ¬ wn 3   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ∖ cdif 3900   ∪ cun 3901

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-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-un 3908

This theorem is referenced by:  dfun3  4227  dfin3  4228