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

Theorem dfin5 3085
 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 3084 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2 df-rab 2427 . 2 {𝑥𝐴𝑥𝐵} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
31, 2eqtr4i 2165 1 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   = wceq 1332   ∈ wcel 1481  {cab 2127  {crab 2422   ∩ cin 3077 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2123 This theorem depends on definitions:  df-bi 116  df-cleq 2134  df-rab 2427  df-in 3084 This theorem is referenced by:  nfin  3289  rabbi2dva  3291  ssfidc  6840  znnen  11983  bj-inex  13321
 Copyright terms: Public domain W3C validator