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

Theorem rabbi2dva 3252
Description: Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
Hypothesis
Ref Expression
rabbi2dva.1 ((𝜑𝑥𝐴) → (𝑥𝐵𝜓))
Assertion
Ref Expression
rabbi2dva (𝜑 → (𝐴𝐵) = {𝑥𝐴𝜓})
Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rabbi2dva
StepHypRef Expression
1 dfin5 3046 . 2 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
2 rabbi2dva.1 . . 3 ((𝜑𝑥𝐴) → (𝑥𝐵𝜓))
32rabbidva 2646 . 2 (𝜑 → {𝑥𝐴𝑥𝐵} = {𝑥𝐴𝜓})
41, 3syl5eq 2160 1 (𝜑 → (𝐴𝐵) = {𝑥𝐴𝜓})
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1314  wcel 1463  {crab 2395  cin 3038
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-ral 2396  df-rab 2400  df-in 3045
This theorem is referenced by:  fndmdif  5491  txcnmpt  12337
  Copyright terms: Public domain W3C validator