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

Theorem abbi2dv 2599
Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
Hypothesis
Ref Expression
abbi2dv.1  |-  ( ph  ->  ( x  e.  A  <->  ps ) )
Assertion
Ref Expression
abbi2dv  |-  ( ph  ->  A  =  { x  |  ps } )
Distinct variable groups:    x, A    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem abbi2dv
StepHypRef Expression
1 abbi2dv.1 . . 3  |-  ( ph  ->  ( x  e.  A  <->  ps ) )
21alrimiv 1690 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  ps )
)
3 abeq2 2586 . 2  |-  ( A  =  { x  |  ps }  <->  A. x
( x  e.  A  <->  ps ) )
42, 3sylibr 212 1  |-  ( ph  ->  A  =  { x  |  ps } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1372    = wceq 1374    e. wcel 1762   {cab 2447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457
This theorem is referenced by:  abbi1dv  2600  sbab  2609  iftrue  3940  iffalse  3943  dfopif  4205  iniseg  5361  fncnvima2  5996  isoini  6215  dftpos3  6965  hartogslem1  7958  r1val2  8246  cardval2  8363  dfac3  8493  wrdval  12506  wrdnval  12526  submacs  15801  dfrhm2  17145  lsppr  17517  rspsn  17679  znunithash  18365  tgval3  19226  txrest  19862  xkoptsub  19885  cnextf  20296  cnblcld  21012  shft2rab  21649  sca2rab  21653  grpoinvf  24906  elpjrn  26773  ofrn2  27141  setlikespec  28832  neibastop3  29772  lkrval2  33764  lshpset2N  33793  hdmapoc  36608
  Copyright terms: Public domain W3C validator