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

Theorem eqabcdv 2876
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
eqabcdv.1 (𝜑 → (𝜓𝑥𝐴))
Assertion
Ref Expression
eqabcdv (𝜑 → {𝑥𝜓} = 𝐴)
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem eqabcdv
StepHypRef Expression
1 eqabcdv.1 . . . 4 (𝜑 → (𝜓𝑥𝐴))
21bicomd 223 . . 3 (𝜑 → (𝑥𝐴𝜓))
32eqabdv 2875 . 2 (𝜑𝐴 = {𝑥𝜓})
43eqcomd 2743 1 (𝜑 → {𝑥𝜓} = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wcel 2108  {cab 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816
This theorem is referenced by:  abidnf  3708  csbtt  3916  csbie2g  3939  csbvarg  4434  iinxsng  5088  predep  6351  fnsnfv  6988  enfin2i  10361  fin1a2lem11  10450  hashf1  14496  shftuz  15108  psrbaglefi  21946  vmappw  27159  addsrid  27997  mulsrid  28139  hdmap1fval  41798  hdmapfval  41829  hgmapfval  41888
  Copyright terms: Public domain W3C validator