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

Theorem dfin4 3900
Description: Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)
Assertion
Ref Expression
dfin4 (𝐴𝐵) = (𝐴 ∖ (𝐴𝐵))

Proof of Theorem dfin4
StepHypRef Expression
1 inss1 3866 . . 3 (𝐴𝐵) ⊆ 𝐴
2 dfss4 3891 . . 3 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵))
31, 2mpbi 220 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵)
4 difin 3894 . . 3 (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)
54difeq2i 3758 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴 ∖ (𝐴𝐵))
63, 5eqtr3i 2675 1 (𝐴𝐵) = (𝐴 ∖ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  cdif 3604  cin 3606  wss 3607
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-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621
This theorem is referenced by:  indif  3902  cnvin  5575  imain  6012  resin  6196  elcls  20925  cmmbl  23348  mbfeqalem  23454  itg1addlem4  23511  itg1addlem5  23512  inelsiga  30326  inelros  30364  topdifinffinlem  33325  poimirlem9  33548  mblfinlem4  33579  ismblfin  33580  cnambfre  33588  stoweidlem50  40585  saliincl  40863  sge0fodjrnlem  40951  meadjiunlem  41000  caragendifcl  41049
  Copyright terms: Public domain W3C validator