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

Theorem dfin5 3959
Description: Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)
Assertion
Ref Expression
dfin5 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfin5
StepHypRef Expression
1 df-in 3958 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 3437 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2768 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1540  wcel 2108  {cab 2714  {crab 3436  cin 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-rab 3437  df-in 3958
This theorem is referenced by:  incom  4209  ineq1  4213  nfinOLD  4225  rabbi2dva  4226  dfss7  4251  dfepfr  5669  epfrc  5670  pmtrmvd  19474  ablfaclem3  20107  mretopd  23100  ptclsg  23623  xkopt  23663  iscmet3  25327  xrlimcnp  27011  ppiub  27248  xppreima  32655  fpwrelmapffs  32745  orvcelval  34471  sstotbnd2  37781  glbconN  39378  glbconNOLD  39379  2polssN  39917  rfovcnvf1od  44017  fsovcnvlem  44026  ntrneifv3  44095  ntrneifv4  44098  clsneifv3  44123  clsneifv4  44124  neicvgfv  44134  inpw  48738
  Copyright terms: Public domain W3C validator