MPE Home 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