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

Theorem abbi2dv 2553
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 1642 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  ps )
)
3 abeq2 2543 . 2  |-  ( A  =  { x  |  ps }  <->  A. x
( x  e.  A  <->  ps ) )
42, 3sylibr 205 1  |-  ( ph  ->  A  =  { x  |  ps } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550    = wceq 1653    e. wcel 1726   {cab 2424
This theorem is referenced by:  sbab  2560  iftrue  3747  iffalse  3748  dfopif  3983  iniseg  5237  fncnvima2  5854  isoini  6060  dftpos3  6499  hartogslem1  7513  r1val2  7765  cardval2  7880  dfac3  8004  wrdval  11732  submacs  14767  dfrhm2  15823  lsppr  16167  rspsn  16327  znunithash  16847  tgval3  17030  txrest  17665  xkoptsub  17688  cnextf  18099  cnblcld  18811  shft2rab  19406  sca2rab  19410  grpoinvf  21830  elpjrn  23695  ofrn2  24055  setlikespec  25464  neibastop3  26393  lkrval2  29950  lshpset2N  29979  hdmapoc  32794
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434
  Copyright terms: Public domain W3C validator