Theorem abbii 2354

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
abbii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
abbii	|- { x | ph } = { x | ps }

Proof of Theorem abbii

Step	Hyp	Ref	Expression
1		abbibcom 2352	. 2 |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
2		abbii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpgbi 1505	1 |- { x | ph } = { x | ps }

Syntax hints:   <-> wb 105   = wceq 1402   {cab 2224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231

This theorem is referenced by:  rabswap  2731  rabbiia  2807  rabab  2843  csb2  3149  cbvcsbw  3151  cbvcsb  3152  csbid  3155  csbco  3157  csbcow  3158  cbvreucsf  3212  unrab  3504  inrab  3505  inrab2  3506  difrab  3507  rabun2  3512  dfnul4  3522  dfnul2  3523  dfnul3  3524  rab0  3551  rabsnifsb  3773  tprot  3800  pw0  3857  dfuni2  3932  unipr  3944  dfint2  3967  int0  3979  dfiunv2  4043  cbviun  4044  cbviin  4045  iunrab  4055  iunid  4063  viin  4067  cbvopab  4197  cbvopab1  4199  cbvopab2  4200  cbvopab1s  4201  cbvopab2v  4203  unopab  4205  iunopab  4419  abnex  4588  uniuni  4592  ruv  4692  rabxp  4807  dfdm3  4962  dfrn2  4963  dfrn3  4964  dfdm4  4968  dfdmf  4969  dmun  4983  dmopab  4987  dmopabss  4988  dmopab3  4989  dfrnf  5018  rnopab  5024  rnmpt  5025  dfima2  5123  dfima3  5124  imadmrn  5131  imai  5138  args  5151  mptpreima  5276  dfiota2  5333  cbviota  5337  cbviotavw  5338  sb8iota  5340  dffv4g  5687  dfimafn2  5746  fnasrn  5878  fnasrng  5880  dfimafnf  5945  elabrex  5953  elabrexg  5954  abrexco  5955  dfoprab2  6125  cbvoprab2  6151  dmoprab  6159  rnoprab  6161  rnoprab2  6162  fnrnov  6225  abrexex2g  6339  abrexex2  6343  abexssex  6344  abexex  6345  oprabrexex2  6353  dfopab2  6413  cnvoprab  6460  cnvimadfsn  6475  tfr1onlemaccex  6609  tfrcllemaccex  6622  tfrcldm  6624  frec0g  6658  frecsuc  6668  snec  6860  pmex  6917  fset0  6939  f1setexg  6941  dfixp  6972  cbvixp  6987  caucvgprprlemmu  8052  caucvgsr  8159  pitonnlem1  8202  hashf1lem2  11264  mertenslem2  12281  4sqlemafi  13152  dfrhm2  14434  toponsspwpwg  15046  tgval2  15075  2lgslem1b  16122  bdcuni  16816  bj-dfom  16873