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

Theorem abbi2dv 2594
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 1720 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  ps )
)
3 abeq2 2581 . 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 1393    = wceq 1395    e. wcel 1819   {cab 2442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452
This theorem is referenced by:  abbi1dv  2595  sbab  2604  iftrue  3950  iffalse  3953  dfopif  4216  iniseg  5378  fncnvima2  6010  isoini  6235  dftpos3  6991  hartogslem1  7985  r1val2  8272  cardval2  8389  dfac3  8519  wrdval  12556  wrdnval  12579  submacs  16123  dfrhm2  17493  lsppr  17866  rspsn  18029  znunithash  18730  tgval3  19591  txrest  20258  xkoptsub  20281  cnextf  20692  cnblcld  21408  shft2rab  22045  sca2rab  22049  grpoinvf  25369  elpjrn  27236  ofrn2  27628  setlikespec  29484  neibastop3  30385  submgmacs  32754  lkrval2  34958  lshpset2N  34987  hdmapoc  37804
  Copyright terms: Public domain W3C validator