Theorem abbii 2323

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

Syntax hints:   <-> wb 105   = wceq 1373   {cab 2193

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200

This theorem is referenced by:  rabswap  2687  rabbiia  2761  rabab  2798  csb2  3103  cbvcsbw  3105  cbvcsb  3106  csbid  3109  csbco  3111  csbcow  3112  cbvreucsf  3166  unrab  3452  inrab  3453  inrab2  3454  difrab  3455  rabun2  3460  dfnul3  3471  rab0  3497  tprot  3736  pw0  3791  dfuni2  3866  unipr  3878  dfint2  3901  int0  3913  dfiunv2  3977  cbviun  3978  cbviin  3979  iunrab  3989  iunid  3997  viin  4001  cbvopab  4131  cbvopab1  4133  cbvopab2  4134  cbvopab1s  4135  cbvopab2v  4137  unopab  4139  iunopab  4346  abnex  4512  uniuni  4516  ruv  4616  rabxp  4730  dfdm3  4883  dfrn2  4884  dfrn3  4885  dfdm4  4889  dfdmf  4890  dmun  4904  dmopab  4908  dmopabss  4909  dmopab3  4910  dfrnf  4938  rnopab  4944  rnmpt  4945  dfima2  5043  dfima3  5044  imadmrn  5051  imai  5057  args  5070  mptpreima  5195  dfiota2  5252  cbviota  5256  sb8iota  5258  dffv4g  5596  dfimafn2  5651  fnasrn  5781  fnasrng  5783  elabrex  5849  elabrexg  5850  abrexco  5851  dfoprab2  6015  cbvoprab2  6041  dmoprab  6049  rnoprab  6051  rnoprab2  6052  fnrnov  6115  abrexex2g  6228  abrexex2  6232  abexssex  6233  abexex  6234  oprabrexex2  6238  dfopab2  6298  cnvoprab  6343  tfr1onlemaccex  6457  tfrcllemaccex  6470  tfrcldm  6472  frec0g  6506  frecsuc  6516  snec  6706  pmex  6763  dfixp  6810  cbvixp  6825  caucvgprprlemmu  7843  caucvgsr  7950  pitonnlem1  7993  mertenslem2  11962  4sqlemafi  12833  dfrhm2  14031  toponsspwpwg  14609  tgval2  14638  2lgslem1b  15681  if0ab  15941  bdcuni  16011  bj-dfom  16068