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

Theorem abbi1dv 2950
 Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
Hypothesis
Ref Expression
abbi1dv.1 (𝜑 → (𝜓𝑥𝐴))
Assertion
Ref Expression
abbi1dv (𝜑 → {𝑥𝜓} = 𝐴)
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem abbi1dv
StepHypRef Expression
1 abbi1dv.1 . . . 4 (𝜑 → (𝜓𝑥𝐴))
21bicomd 226 . . 3 (𝜑 → (𝑥𝐴𝜓))
32abbi2dv 2949 . 2 (𝜑𝐴 = {𝑥𝜓})
43eqcomd 2827 1 (𝜑 → {𝑥𝜓} = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2115  {cab 2799 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892 This theorem is referenced by:  abidnf  3671  csbtt  3874  csbie2g  3897  csbvarg  4356  iinxsng  4983  predep  6147  enfin2i  9720  fin1a2lem11  9809  hashf1  13799  shftuz  14407  psrbaglefi  20127  vmappw  25679  hdmap1fval  38972  hdmapfval  39003  hgmapfval  39062  rabeqcda  39222
 Copyright terms: Public domain W3C validator