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

Theorem dfin4 3998
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 3964 . . 3 (𝐴𝐵) ⊆ 𝐴
2 dfss4 3989 . . 3 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵))
31, 2mpbi 220 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵)
4 difin 3992 . . 3 (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)
54difeq2i 3856 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴 ∖ (𝐴𝐵))
63, 5eqtr3i 2772 1 (𝐴𝐵) = (𝐴 ∖ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1620  cdif 3700  cin 3702  wss 3703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rab 3047  df-v 3330  df-dif 3706  df-in 3710  df-ss 3717
This theorem is referenced by:  indif  4000  cnvin  5686  imain  6123  resin  6307  elcls  21050  cmmbl  23473  mbfeqalem  23579  itg1addlem4  23636  itg1addlem5  23637  inelsiga  30478  inelros  30516  topdifinffinlem  33477  poimirlem9  33700  mblfinlem4  33731  ismblfin  33732  cnambfre  33740  stoweidlem50  40739  saliincl  41017  sge0fodjrnlem  41105  meadjiunlem  41154  caragendifcl  41203
  Copyright terms: Public domain W3C validator