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

Theorem abbi1dv 2881
 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 213 . . 3 (𝜑 → (𝑥𝐴𝜓))
32abbi2dv 2880 . 2 (𝜑𝐴 = {𝑥𝜓})
43eqcomd 2766 1 (𝜑 → {𝑥𝜓} = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2139  {cab 2746 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756 This theorem is referenced by:  abidnf  3516  csbtt  3685  csbie2g  3705  csbvarg  4146  iinxsng  4752  predep  5867  enfin2i  9355  fin1a2lem11  9444  hashf1  13453  shftuz  14028  psrbaglefi  19594  vmappw  25062  hdmap1fval  37606  hdmapfval  37639  hgmapfval  37698
 Copyright terms: Public domain W3C validator