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

Theorem dfin2 4212
Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4211. Another version is given by dfin4 4219. (Contributed by NM, 10-Jun-2004.)
Assertion
Ref Expression
dfin2 (𝐴𝐵) = (𝐴 ∖ (V ∖ 𝐵))

Proof of Theorem dfin2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 vex 3474 . . . . . 6 𝑥 ∈ V
2 eldif 3920 . . . . . 6 (𝑥 ∈ (V ∖ 𝐵) ↔ (𝑥 ∈ V ∧ ¬ 𝑥𝐵))
31, 2mpbiran 708 . . . . 5 (𝑥 ∈ (V ∖ 𝐵) ↔ ¬ 𝑥𝐵)
43con2bii 361 . . . 4 (𝑥𝐵 ↔ ¬ 𝑥 ∈ (V ∖ 𝐵))
54anbi2i 625 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
6 eldif 3920 . . 3 (𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
75, 6bitr4i 281 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)))
87ineqri 4155 1 (𝐴𝐵) = (𝐴 ∖ (V ∖ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 399   = wceq 1538  wcel 2115  Vcvv 3471  cdif 3907  cin 3909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-dif 3913  df-in 3917
This theorem is referenced by:  dfun3  4217  dfin3  4218  invdif  4220  difundi  4231  difindi  4233  difdif2  4236
  Copyright terms: Public domain W3C validator