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

Theorem dfin5 3923
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 3922 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 3411 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2768 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
Colors of variables: wff setvar class
Syntax hints:  wa 397   = wceq 1542  wcel 2107  {cab 2714  {crab 3410  cin 3914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-rab 3411  df-in 3922
This theorem is referenced by:  incom  4166  ineq1  4170  nfin  4181  rabbi2dva  4182  dfss7  4205  dfepfr  5623  epfrc  5624  pmtrmvd  19245  ablfaclem3  19873  mretopd  22459  ptclsg  22982  xkopt  23022  iscmet3  24673  xrlimcnp  26334  ppiub  26568  xppreima  31604  fpwrelmapffs  31693  orvcelval  33108  sstotbnd2  36262  glbconN  37868  glbconNOLD  37869  2polssN  38407  rfovcnvf1od  42350  fsovcnvlem  42359  ntrneifv3  42428  ntrneifv4  42431  clsneifv3  42456  clsneifv4  42457  neicvgfv  42467  inpw  46977
  Copyright terms: Public domain W3C validator