Theorem abbii 2194

Description: Equivalent wff's yield equal class abstractions (inference rule). (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 2192	. 2 |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
2		abbii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpgbi 1381	1 |- { x | ph } = { x | ps }

Syntax hints:   <-> wb 103   = wceq 1284   {cab 2067

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074

This theorem is referenced by:  rabswap  2532  rabbiia  2591  rabab  2620  csb2  2910  cbvcsb  2912  csbid  2915  csbco  2917  cbvreucsf  2966  unrab  3235  inrab  3236  inrab2  3237  difrab  3238  rabun2  3243  dfnul3  3254  rab0  3273  tprot  3485  pw0  3532  dfuni2  3603  unipr  3615  dfint2  3638  int0  3650  dfiunv2  3714  cbviun  3715  cbviin  3716  iunrab  3725  iunid  3733  viin  3737  cbvopab  3849  cbvopab1  3851  cbvopab2  3852  cbvopab1s  3853  cbvopab2v  3855  unopab  3857  iunopab  4036  uniuni  4201  ruv  4293  rabxp  4398  dfdm3  4540  dfrn2  4541  dfrn3  4542  dfdm4  4545  dfdmf  4546  dmun  4560  dmopab  4564  dmopabss  4565  dmopab3  4566  dfrnf  4593  rnopab  4599  rnmpt  4600  dfima2  4690  dfima3  4691  imadmrn  4698  imai  4701  args  4714  mptpreima  4834  dfiota2  4888  cbviota  4892  sb8iota  4894  dffv4g  5195  dfimafn2  5244  fnasrn  5362  fnasrng  5364  elabrex  5418  abrexco  5419  dfoprab2  5572  cbvoprab2  5597  dmoprab  5605  rnoprab  5607  rnoprab2  5608  fnrnov  5666  abrexex2g  5767  abrexex2  5771  abexssex  5772  abexex  5773  oprabrexex2  5777  dfopab2  5835  cnvoprab  5875  frec0g  6006  frecsuc  6014  snec  6190  caucvgprprlemmu  6885  caucvgsr  6978  pitonnlem1  7013  bdcuni  10667  bj-dfom  10728