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

Theorem abbi2dv 2400
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 1619 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  ps )
)
3 abeq2 2390 . 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 1529    = wceq 1625    e. wcel 1686   {cab 2271
This theorem is referenced by:  sbab  2407  iftrue  3573  iffalse  3574  dfopif  3795  iniseg  5046  fncnvima2  5649  isoini  5837  dftpos3  6254  hartogslem1  7259  r1val2  7511  cardval2  7626  dfac3  7750  wrdval  11418  submacs  14444  dfrhm2  15500  lsppr  15848  rspsn  16008  znunithash  16520  tgval3  16703  txrest  17327  xkoptsub  17350  cnblcld  18286  shft2rab  18869  sca2rab  18873  grpoinvf  20909  elpjrn  22772  setlikespec  24189  prj1b  25090  prj3  25091  repcpwti  25172  nZdef  25191  neibastop3  26322  lkrval2  29353  lshpset2N  29382  hdmapoc  32197
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281
  Copyright terms: Public domain W3C validator