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

Theorem abbi2dv 2411
Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
Hypothesis
Ref Expression
abbirdv.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 abbirdv.1 . . 3  |-  ( ph  ->  ( x  e.  A  <->  ps ) )
21alrimiv 1621 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  ps )
)
3 abeq2 2401 . 2  |-  ( A  =  { x  |  ps }  <->  A. x
( x  e.  A  <->  ps ) )
42, 3sylibr 203 1  |-  ( ph  ->  A  =  { x  |  ps } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530    = wceq 1632    e. wcel 1696   {cab 2282
This theorem is referenced by:  sbab  2418  iftrue  3584  iffalse  3585  dfopif  3809  iniseg  5060  fncnvima2  5663  isoini  5851  dftpos3  6268  hartogslem1  7273  r1val2  7525  cardval2  7640  dfac3  7764  wrdval  11432  submacs  14458  dfrhm2  15514  lsppr  15862  rspsn  16022  znunithash  16534  tgval3  16717  txrest  17341  xkoptsub  17364  cnblcld  18300  shft2rab  18883  sca2rab  18887  grpoinvf  20923  elpjrn  22786  setlikespec  24258  prj1b  25182  prj3  25183  repcpwti  25264  nZdef  25283  neibastop3  26414  lkrval2  29902  lshpset2N  29931  hdmapoc  32746
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator