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

Theorem dfin5 3947
 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 3946 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 3151 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2851 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 396   = wceq 1530   ∈ wcel 2107  {cab 2803  {crab 3146   ∩ cin 3938 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2797 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2818  df-rab 3151  df-in 3946 This theorem is referenced by:  incom  4181  ineq1  4184  nfin  4196  rabbi2dva  4197  dfss7  4220  dfepfr  5538  epfrc  5539  pmtrmvd  18506  ablfaclem3  19131  mretopd  21618  ptclsg  22141  xkopt  22181  iscmet3  23813  xrlimcnp  25462  ppiub  25696  xppreima  30311  fpwrelmapffs  30385  orvcelval  31614  sstotbnd2  34922  glbconN  36382  2polssN  36920  rfovcnvf1od  40217  fsovcnvlem  40226  ntrneifv3  40299  ntrneifv4  40302  clsneifv3  40327  clsneifv4  40328  neicvgfv  40338
 Copyright terms: Public domain W3C validator