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

Theorem dfin5 3952
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 3951 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 3432 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2762 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1541  wcel 2106  {cab 2708  {crab 3431  cin 3943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-rab 3432  df-in 3951
This theorem is referenced by:  incom  4197  ineq1  4201  nfin  4212  rabbi2dva  4213  dfss7  4236  dfepfr  5654  epfrc  5655  pmtrmvd  19288  ablfaclem3  19916  mretopd  22525  ptclsg  23048  xkopt  23088  iscmet3  24739  xrlimcnp  26400  ppiub  26634  xppreima  31740  fpwrelmapffs  31830  orvcelval  33298  sstotbnd2  36447  glbconN  38052  glbconNOLD  38053  2polssN  38591  rfovcnvf1od  42526  fsovcnvlem  42535  ntrneifv3  42604  ntrneifv4  42607  clsneifv3  42632  clsneifv4  42633  neicvgfv  42643  inpw  47151
  Copyright terms: Public domain W3C validator