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

Theorem abbi2dv 2550
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 1641 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  ps )
)
3 abeq2 2540 . 2  |-  ( A  =  { x  |  ps }  <->  A. x
( x  e.  A  <->  ps ) )
42, 3sylibr 204 1  |-  ( ph  ->  A  =  { x  |  ps } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549    = wceq 1652    e. wcel 1725   {cab 2421
This theorem is referenced by:  sbab  2557  iftrue  3737  iffalse  3738  dfopif  3973  iniseg  5227  fncnvima2  5844  isoini  6050  dftpos3  6489  hartogslem1  7503  r1val2  7755  cardval2  7870  dfac3  7994  wrdval  11722  submacs  14757  dfrhm2  15813  lsppr  16157  rspsn  16317  znunithash  16837  tgval3  17020  txrest  17655  xkoptsub  17678  cnextf  18089  cnblcld  18801  shft2rab  19396  sca2rab  19400  grpoinvf  21820  elpjrn  23685  ofrn2  24045  setlikespec  25454  neibastop3  26382  lkrval2  29825  lshpset2N  29854  hdmapoc  32669
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator