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