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

Theorem abbi2dv 2728
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 1841 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
3 abeq2 2718 . 2 (𝐴 = {𝑥𝜓} ↔ ∀𝑥(𝑥𝐴𝜓))
42, 3sylibr 222 1 (𝜑𝐴 = {𝑥𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472   = wceq 1474  wcel 1976  {cab 2595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605
This theorem is referenced by:  abbi1dv  2729  sbab  2736  iftrue  4041  iffalse  4044  dfopif  4331  iniseg  5401  setlikespec  5603  fncnvima2  6231  isoini  6465  dftpos3  7234  hartogslem1  8307  r1val2  8560  cardval2  8677  dfac3  8804  wrdval  13111  wrdnval  13138  submacs  17136  dfrhm2  18488  lsppr  18862  rspsn  19023  znunithash  19679  tgval3  20525  txrest  21191  xkoptsub  21214  cnextf  21627  cnblcld  22335  shft2rab  23027  sca2rab  23031  grpoinvf  26563  elpjrn  28226  ofrn2  28615  neibastop3  31320  lkrval2  33178  lshpset2N  33207  hdmapoc  36024  mapsnd  38166  submgmacs  41575
  Copyright terms: Public domain W3C validator