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

Theorem dfin4 4097
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 4057 . . 3 (𝐴𝐵) ⊆ 𝐴
2 dfss4 4088 . . 3 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵))
31, 2mpbi 222 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵)
4 difin 4091 . . 3 (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)
54difeq2i 3952 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴 ∖ (𝐴𝐵))
63, 5eqtr3i 2851 1 (𝐴𝐵) = (𝐴 ∖ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1658  cdif 3795  cin 3797  wss 3798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rab 3126  df-v 3416  df-dif 3801  df-in 3805  df-ss 3812
This theorem is referenced by:  indif  4099  cnvin  5781  imain  6207  resin  6399  elcls  21248  cmmbl  23700  mbfeqalem2  23808  itg1addlem4  23865  itg1addlem5  23866  inelsiga  30743  inelros  30781  topdifinffinlem  33740  poimirlem9  33962  mblfinlem4  33993  ismblfin  33994  cnambfre  34001  stoweidlem50  41061  saliincl  41336  sge0fodjrnlem  41424  meadjiunlem  41473  caragendifcl  41522
  Copyright terms: Public domain W3C validator