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 }

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402   {cab 2224

This proof depends on 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 proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231

This theorem is used 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  3777  tprot  3804  pw0  3862  dfuni2  3937  unipr  3949  dfint2  3972  int0  3984  dfiunv2  4048  cbviun  4049  cbviin  4050  iunrab  4060  iunid  4068  viin  4072  cbvopab  4203  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  cbvopab2v  4209  unopab  4211  iunopab  4426  abnex  4595  uniuni  4599  ruv  4699  rabxp  4814  dfdm3  4969  dfrn2  4970  dfrn3  4971  dfdm4  4975  dfdmf  4976  dmun  4990  dmopab  4994  dmopabss  4995  dmopab3  4996  dfrnf  5025  rnopab  5031  rnmpt  5032  dfima2  5131  dfima3  5132  imadmrn  5139  imai  5146  args  5159  mptpreima  5284  dfiota2  5341  cbviota  5345  cbviotavw  5346  sb8iota  5348  dffv4g  5695  dfimafn2  5755  fnasrn  5890  fnasrng  5892  dfimafnf  5958  elabrex  5966  elabrexg  5967  abrexco  5968  dfoprab2  6138  cbvoprab2  6164  dmoprab  6172  rnoprab  6174  rnoprab2  6175  fnrnov  6238  abrexex2g  6353  abrexex2  6357  abexssex  6358  abexex  6359  oprabrexex2  6367  dfopab2  6427  cnvoprab  6474  cnvimadfsn  6489  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfrcldm  6638  frec0g  6672  frecsuc  6682  snec  6874  pmex  6931  fset0  6953  f1setexg  6955  dfixp  6986  cbvixp  7001  caucvgprprlemmu  8068  caucvgsr  8175  pitonnlem1  8218  hashf1lem2  11308  mertenslem2  12328  4sqlemafi  13203  dfrhm2  14570  toponsspwpwg  15248  tgval2  15277  2lgslem1b  16413  bdcuni  17107  bj-dfom  17164