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

Theorem abbi2dv 2588
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 1686 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  ps )
)
3 abeq2 2575 . 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 1368    = wceq 1370    e. wcel 1758   {cab 2436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446
This theorem is referenced by:  abbi1dv  2589  sbab  2598  iftrue  3897  iffalse  3899  dfopif  4156  iniseg  5300  fncnvima2  5926  isoini  6130  dftpos3  6865  hartogslem1  7859  r1val2  8147  cardval2  8264  dfac3  8394  wrdval  12342  submacs  15597  dfrhm2  16916  lsppr  17282  rspsn  17444  znunithash  18108  tgval3  18686  txrest  19322  xkoptsub  19345  cnextf  19756  cnblcld  20472  shft2rab  21109  sca2rab  21113  grpoinvf  23864  elpjrn  25731  ofrn2  26094  setlikespec  27784  neibastop3  28723  wrdnval  30614  lkrval2  33043  lshpset2N  33072  hdmapoc  35887
  Copyright terms: Public domain W3C validator