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

Theorem dfin5 3723
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 3722 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 3059 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2785 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1632  wcel 2139  {cab 2746  {crab 3054  cin 3714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-rab 3059  df-in 3722
This theorem is referenced by:  nfin  3963  rabbi2dva  3964  dfepfr  5251  epfrc  5252  pmtrmvd  18076  ablfaclem3  18686  mretopd  21098  ptclsg  21620  xkopt  21660  iscmet3  23291  xrlimcnp  24894  ppiub  25128  xppreima  29758  fpwrelmapffs  29818  orvcelval  30839  sstotbnd2  33886  glbconN  35166  2polssN  35704  rfovcnvf1od  38800  fsovcnvlem  38809  ntrneifv3  38882  ntrneifv4  38885  clsneifv3  38910  clsneifv4  38911  neicvgfv  38921
  Copyright terms: Public domain W3C validator