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

Theorem dfin5 3548
 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 3547 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 2905 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2635 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  {crab 2900   ∩ cin 3539 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-rab 2905  df-in 3547 This theorem is referenced by:  nfin  3782  rabbi2dva  3783  dfepfr  5023  epfrc  5024  pmtrmvd  17699  ablfaclem3  18309  mretopd  20706  ptclsg  21228  xkopt  21268  iscmet3  22899  xrlimcnp  24495  ppiub  24729  xppreima  28829  fpwrelmapffs  28897  orvcelval  29857  sstotbnd2  32743  glbconN  33681  2polssN  34219  rfovcnvf1od  37318  fsovcnvlem  37327  ntrneifv3  37400  ntrneifv4  37403  clsneifv3  37428  clsneifv4  37429  neicvgfv  37439
 Copyright terms: Public domain W3C validator