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

Theorem abbi2dv 2926
Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
Hypothesis
Ref Expression
abbi2dv.1 (𝜑 → (𝑥𝐴𝜓))
Assertion
Ref Expression
abbi2dv (𝜑𝐴 = {𝑥𝜓})
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem abbi2dv
StepHypRef Expression
1 abbi2dv.1 . . 3 (𝜑 → (𝑥𝐴𝜓))
21alrimiv 2018 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
3 abeq2 2916 . 2 (𝐴 = {𝑥𝜓} ↔ ∀𝑥(𝑥𝐴𝜓))
42, 3sylibr 225 1 (𝜑𝐴 = {𝑥𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1635   = wceq 1637  wcel 2156  {cab 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802
This theorem is referenced by:  abbi1dv  2927  sbab  2934  iftrue  4285  iffalse  4288  dfopif  4592  iniseg  5706  setlikespec  5914  fncnvima2  6561  isoini  6812  dftpos3  7605  mapsnd  8134  hartogslem1  8686  r1val2  8947  cardval2  9100  dfac3  9227  wrdval  13519  wrdnval  13546  submacs  17570  dfrhm2  18921  lsppr  19300  rspsn  19463  znunithash  20120  tgval3  20981  txrest  21648  xkoptsub  21671  cnextf  22083  cnblcld  22791  shft2rab  23489  sca2rab  23493  grpoinvf  27715  elpjrn  29377  ofrn2  29769  neibastop3  32678  ecres2  34361  lkrval2  34870  lshpset2N  34899  hdmapoc  37712  submgmacs  42372
  Copyright terms: Public domain W3C validator