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

Theorem abbi2dv 2889
 Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2158. (Revised by Wolf Lammen, 6-May-2023.)
Hypothesis
Ref Expression
abbi2dv.1 (𝜑 → (𝑥𝐴𝜓))
Assertion
Ref Expression
abbi2dv (𝜑𝐴 = {𝑥𝜓})
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem abbi2dv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 abbi2dv.1 . . . 4 (𝜑 → (𝑥𝐴𝜓))
21sbbidv 2084 . . 3 (𝜑 → ([𝑦 / 𝑥]𝑥𝐴 ↔ [𝑦 / 𝑥]𝜓))
3 clelsb3 2879 . . . 4 ([𝑦 / 𝑥]𝑥𝐴𝑦𝐴)
43bicomi 227 . . 3 (𝑦𝐴 ↔ [𝑦 / 𝑥]𝑥𝐴)
5 df-clab 2736 . . 3 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
62, 4, 53bitr4g 317 . 2 (𝜑 → (𝑦𝐴𝑦 ∈ {𝑥𝜓}))
76eqrdv 2756 1 (𝜑𝐴 = {𝑥𝜓})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  [wsb 2069   ∈ wcel 2111  {cab 2735 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830 This theorem is referenced by:  abbi1dv  2890  abbi2i  2891  sbab  2898  iftrue  4429  iffalse  4432  dfopifOLD  4761  iniseg  5937  setlikespec  6152  fncnvima2  6827  isoini  7091  dftpos3  7926  mapsnd  8481  hartogslem1  9052  r1val2  9312  cardval2  9466  dfac3  9594  wrdval  13929  wrdnval  13957  submacs  18070  ablsimpgfind  19313  dfrhm2  19553  lsppr  19946  rspsn  20108  znunithash  20345  tgval3  21676  txrest  22344  xkoptsub  22367  cnextf  22779  cnblcld  23489  shft2rab  24221  sca2rab  24225  grpoinvf  28427  elpjrn  30085  ofrn2  30512  addscllem1  33714  neibastop3  34134  ecres2  36010  lkrval2  36700  lshpset2N  36729  hdmapoc  39541  submgmacs  44840
 Copyright terms: Public domain W3C validator