ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfin5 GIF version

Theorem dfin5 2995
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 2994 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 2364 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2108 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
Colors of variables: wff set class
Syntax hints:  wa 102   = wceq 1287  wcel 1436  {cab 2071  {crab 2359  cin 2987
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-rab 2364  df-in 2994
This theorem is referenced by:  nfin  3195  rabbi2dva  3197  ssfidc  6594  znnen  11093  bj-inex  11243
  Copyright terms: Public domain W3C validator