Theorem abbii 2282

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

Syntax hints:   <-> wb 104   = wceq 1343   {cab 2151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158

This theorem is referenced by:  rabswap  2644  rabbiia  2711  rabab  2747  csb2  3047  cbvcsbw  3049  cbvcsb  3050  csbid  3053  csbco  3055  csbcow  3056  cbvreucsf  3109  unrab  3393  inrab  3394  inrab2  3395  difrab  3396  rabun2  3401  dfnul3  3412  rab0  3437  tprot  3669  pw0  3720  dfuni2  3791  unipr  3803  dfint2  3826  int0  3838  dfiunv2  3902  cbviun  3903  cbviin  3904  iunrab  3913  iunid  3921  viin  3925  cbvopab  4053  cbvopab1  4055  cbvopab2  4056  cbvopab1s  4057  cbvopab2v  4059  unopab  4061  iunopab  4259  abnex  4425  uniuni  4429  ruv  4527  rabxp  4641  dfdm3  4791  dfrn2  4792  dfrn3  4793  dfdm4  4796  dfdmf  4797  dmun  4811  dmopab  4815  dmopabss  4816  dmopab3  4817  dfrnf  4845  rnopab  4851  rnmpt  4852  dfima2  4948  dfima3  4949  imadmrn  4956  imai  4960  args  4973  mptpreima  5097  dfiota2  5154  cbviota  5158  sb8iota  5160  dffv4g  5483  dfimafn2  5536  fnasrn  5663  fnasrng  5665  elabrex  5726  abrexco  5727  dfoprab2  5889  cbvoprab2  5915  dmoprab  5923  rnoprab  5925  rnoprab2  5926  fnrnov  5987  abrexex2g  6088  abrexex2  6092  abexssex  6093  abexex  6094  oprabrexex2  6098  dfopab2  6157  cnvoprab  6202  tfr1onlemaccex  6316  tfrcllemaccex  6329  tfrcldm  6331  frec0g  6365  frecsuc  6375  snec  6562  pmex  6619  dfixp  6666  cbvixp  6681  caucvgprprlemmu  7636  caucvgsr  7743  pitonnlem1  7786  mertenslem2  11477  toponsspwpwg  12660  tgval2  12691  if0ab  13687  bdcuni  13758  bj-dfom  13815