MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfun2 Structured version   Visualization version   GIF version

Theorem dfun2 4270
Description: An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4271 and dfss4 4269 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.
StepHypRef Expression
1 vex 3484 . . . . . . 7 𝑥 ∈ V
2 eldif 3961 . . . . . . 7 (𝑥 ∈ (V ∖ 𝐴) ↔ (𝑥 ∈ V ∧ ¬ 𝑥𝐴))
31, 2mpbiran 709 . . . . . 6 (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥𝐴)
43anbi1i 624 . . . . 5 ((𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥𝐵) ↔ (¬ 𝑥𝐴 ∧ ¬ 𝑥𝐵))
5 eldif 3961 . . . . 5 (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ (𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥𝐵))
6 ioran 986 . . . . 5 (¬ (𝑥𝐴𝑥𝐵) ↔ (¬ 𝑥𝐴 ∧ ¬ 𝑥𝐵))
74, 5, 63bitr4i 303 . . . 4 (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ ¬ (𝑥𝐴𝑥𝐵))
87con2bii 357 . . 3 ((𝑥𝐴𝑥𝐵) ↔ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵))
9 eldif 3961 . . . 4 (𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵)))
101, 9mpbiran 709 . . 3 (𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) ↔ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵))
118, 10bitr4i 278 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)))
1211uneqri 4156 1 (𝐴𝐵) = (V ∖ ((V ∖ 𝐴) ∖ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395  wo 848   = wceq 1540  wcel 2108  Vcvv 3480  cdif 3948  cun 3949
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956
This theorem is referenced by:  dfun3  4276  dfin3  4277
  Copyright terms: Public domain W3C validator