Theorem abbii 2256

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

Syntax hints:   <-> wb 104   = wceq 1332   {cab 2126

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133

This theorem is referenced by:  rabswap  2612  rabbiia  2674  rabab  2710  csb2  3009  cbvcsbw  3011  cbvcsb  3012  csbid  3015  csbco  3017  cbvreucsf  3069  unrab  3352  inrab  3353  inrab2  3354  difrab  3355  rabun2  3360  dfnul3  3371  rab0  3396  tprot  3624  pw0  3675  dfuni2  3746  unipr  3758  dfint2  3781  int0  3793  dfiunv2  3857  cbviun  3858  cbviin  3859  iunrab  3868  iunid  3876  viin  3880  cbvopab  4007  cbvopab1  4009  cbvopab2  4010  cbvopab1s  4011  cbvopab2v  4013  unopab  4015  iunopab  4211  abnex  4376  uniuni  4380  ruv  4473  rabxp  4584  dfdm3  4734  dfrn2  4735  dfrn3  4736  dfdm4  4739  dfdmf  4740  dmun  4754  dmopab  4758  dmopabss  4759  dmopab3  4760  dfrnf  4788  rnopab  4794  rnmpt  4795  dfima2  4891  dfima3  4892  imadmrn  4899  imai  4903  args  4916  mptpreima  5040  dfiota2  5097  cbviota  5101  sb8iota  5103  dffv4g  5426  dfimafn2  5479  fnasrn  5606  fnasrng  5608  elabrex  5667  abrexco  5668  dfoprab2  5826  cbvoprab2  5852  dmoprab  5860  rnoprab  5862  rnoprab2  5863  fnrnov  5924  abrexex2g  6026  abrexex2  6030  abexssex  6031  abexex  6032  oprabrexex2  6036  dfopab2  6095  cnvoprab  6139  tfr1onlemaccex  6253  tfrcllemaccex  6266  tfrcldm  6268  frec0g  6302  frecsuc  6312  snec  6498  pmex  6555  dfixp  6602  cbvixp  6617  caucvgprprlemmu  7527  caucvgsr  7634  pitonnlem1  7677  mertenslem2  11337  toponsspwpwg  12228  tgval2  12259  bdcuni  13245  bj-dfom  13302