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

Theorem dfin2 3893
Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 3892. Another version is given by dfin4 3900. (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 3234 . . . . . 6 𝑥 ∈ V
2 eldif 3617 . . . . . 6 (𝑥 ∈ (V ∖ 𝐵) ↔ (𝑥 ∈ V ∧ ¬ 𝑥𝐵))
31, 2mpbiran 973 . . . . 5 (𝑥 ∈ (V ∖ 𝐵) ↔ ¬ 𝑥𝐵)
43con2bii 346 . . . 4 (𝑥𝐵 ↔ ¬ 𝑥 ∈ (V ∖ 𝐵))
54anbi2i 730 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
6 eldif 3617 . . 3 (𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵)))
75, 6bitr4i 267 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)))
87ineqri 3839 1 (𝐴𝐵) = (𝐴 ∖ (V ∖ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 383   = wceq 1523  wcel 2030  Vcvv 3231  cdif 3604  cin 3606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-in 3614
This theorem is referenced by:  dfun3  3898  dfin3  3899  invdif  3901  difundi  3912  difindi  3914  difdif2  3917
  Copyright terms: Public domain W3C validator