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

Theorem abbi2dv 2771
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 1895 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
3 abeq2 2761 . 2 (𝐴 = {𝑥𝜓} ↔ ∀𝑥(𝑥𝐴𝜓))
42, 3sylibr 224 1 (𝜑𝐴 = {𝑥𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521   = wceq 1523  wcel 2030  {cab 2637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647
This theorem is referenced by:  abbi1dv  2772  sbab  2779  iftrue  4125  iffalse  4128  dfopif  4430  iniseg  5531  setlikespec  5739  fncnvima2  6379  isoini  6628  dftpos3  7415  hartogslem1  8488  r1val2  8738  cardval2  8855  dfac3  8982  wrdval  13340  wrdnval  13367  submacs  17412  dfrhm2  18765  lsppr  19141  rspsn  19302  znunithash  19961  tgval3  20815  txrest  21482  xkoptsub  21505  cnextf  21917  cnblcld  22625  shft2rab  23322  sca2rab  23326  grpoinvf  27514  elpjrn  29177  ofrn2  29570  neibastop3  32482  ecres2  34185  lkrval2  34695  lshpset2N  34724  hdmapoc  37540  mapsnd  39702  submgmacs  42129
  Copyright terms: Public domain W3C validator