Theorem dfun2 4275

Description: An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4276 and dfss4 4274 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 3481	. . . . . . 7 ⊢ 𝑥 ∈ V
2		eldif 3972	. . . . . . 7 ⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐴))
3	1, 2	mpbiran 709	. . . . . 6 ⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴)
4	3	anbi1i 624	. . . . 5 ⊢ ((𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
5		eldif 3972	. . . . 5 ⊢ (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ (𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥 ∈ 𝐵))
6		ioran 985	. . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
7	4, 5, 6	3bitr4i 303	. . . 4 ⊢ (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
8	7	con2bii 357	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵))
9		eldif 3972	. . . 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 4165	1 ⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∖ 𝐵))

Syntax hints:  ¬ wn 3   ∧ wa 395   ∨ wo 847   = wceq 1536   ∈ wcel 2105  Vcvv 3477   ∖ cdif 3959   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967

This theorem is referenced by:  dfun3  4281  dfin3  4282