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

Theorem dfin5 3547
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 3546 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 2904 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2634 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wcel 1976  {cab 2595  {crab 2899  cin 3538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-rab 2904  df-in 3546
This theorem is referenced by:  nfin  3781  rabbi2dva  3782  dfepfr  5013  epfrc  5014  pmtrmvd  17645  ablfaclem3  18255  mretopd  20648  ptclsg  21170  xkopt  21210  iscmet3  22817  xrlimcnp  24412  ppiub  24646  xppreima  28635  fpwrelmapffs  28703  orvcelval  29663  sstotbnd2  32539  glbconN  33477  2polssN  34015  rfovcnvf1od  37114  fsovcnvlem  37123  ntrneifv3  37196  ntrneifv4  37199  clsneifv3  37224  clsneifv4  37225  neicvgfv  37235
  Copyright terms: Public domain W3C validator