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

Theorem dfin5 3711
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 3710 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 3047 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2773 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1620  wcel 2127  {cab 2734  {crab 3042  cin 3702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1842  df-cleq 2741  df-rab 3047  df-in 3710
This theorem is referenced by:  nfin  3951  rabbi2dva  3952  dfepfr  5239  epfrc  5240  pmtrmvd  18047  ablfaclem3  18657  mretopd  21069  ptclsg  21591  xkopt  21631  iscmet3  23262  xrlimcnp  24865  ppiub  25099  xppreima  29729  fpwrelmapffs  29789  orvcelval  30810  sstotbnd2  33855  glbconN  35135  2polssN  35673  rfovcnvf1od  38769  fsovcnvlem  38778  ntrneifv3  38851  ntrneifv4  38854  clsneifv3  38879  clsneifv4  38880  neicvgfv  38890
  Copyright terms: Public domain W3C validator