Theorem abbii 2293

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		abbi 2291	. 2 |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
2		abbii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpgbi 1452	1 |- { x | ph } = { x | ps }

Syntax hints:   <-> wb 105   = wceq 1353   {cab 2163

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170

This theorem is referenced by:  rabswap  2655  rabbiia  2722  rabab  2758  csb2  3059  cbvcsbw  3061  cbvcsb  3062  csbid  3065  csbco  3067  csbcow  3068  cbvreucsf  3121  unrab  3406  inrab  3407  inrab2  3408  difrab  3409  rabun2  3414  dfnul3  3425  rab0  3451  tprot  3685  pw0  3739  dfuni2  3811  unipr  3823  dfint2  3846  int0  3858  dfiunv2  3922  cbviun  3923  cbviin  3924  iunrab  3934  iunid  3942  viin  3946  cbvopab  4074  cbvopab1  4076  cbvopab2  4077  cbvopab1s  4078  cbvopab2v  4080  unopab  4082  iunopab  4281  abnex  4447  uniuni  4451  ruv  4549  rabxp  4663  dfdm3  4814  dfrn2  4815  dfrn3  4816  dfdm4  4819  dfdmf  4820  dmun  4834  dmopab  4838  dmopabss  4839  dmopab3  4840  dfrnf  4868  rnopab  4874  rnmpt  4875  dfima2  4972  dfima3  4973  imadmrn  4980  imai  4984  args  4997  mptpreima  5122  dfiota2  5179  cbviota  5183  sb8iota  5185  dffv4g  5512  dfimafn2  5565  fnasrn  5694  fnasrng  5696  elabrex  5758  abrexco  5759  dfoprab2  5921  cbvoprab2  5947  dmoprab  5955  rnoprab  5957  rnoprab2  5958  fnrnov  6019  abrexex2g  6120  abrexex2  6124  abexssex  6125  abexex  6126  oprabrexex2  6130  dfopab2  6189  cnvoprab  6234  tfr1onlemaccex  6348  tfrcllemaccex  6361  tfrcldm  6363  frec0g  6397  frecsuc  6407  snec  6595  pmex  6652  dfixp  6699  cbvixp  6714  caucvgprprlemmu  7693  caucvgsr  7800  pitonnlem1  7843  mertenslem2  11543  toponsspwpwg  13492  tgval2  13521  if0ab  14527  bdcuni  14598  bj-dfom  14655