Theorem abbii 2321

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

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

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198

This theorem is referenced by:  rabswap  2685  rabbiia  2757  rabab  2793  csb2  3095  cbvcsbw  3097  cbvcsb  3098  csbid  3101  csbco  3103  csbcow  3104  cbvreucsf  3158  unrab  3444  inrab  3445  inrab2  3446  difrab  3447  rabun2  3452  dfnul3  3463  rab0  3489  tprot  3726  pw0  3780  dfuni2  3852  unipr  3864  dfint2  3887  int0  3899  dfiunv2  3963  cbviun  3964  cbviin  3965  iunrab  3975  iunid  3983  viin  3987  cbvopab  4115  cbvopab1  4117  cbvopab2  4118  cbvopab1s  4119  cbvopab2v  4121  unopab  4123  iunopab  4328  abnex  4494  uniuni  4498  ruv  4598  rabxp  4712  dfdm3  4865  dfrn2  4866  dfrn3  4867  dfdm4  4870  dfdmf  4871  dmun  4885  dmopab  4889  dmopabss  4890  dmopab3  4891  dfrnf  4919  rnopab  4925  rnmpt  4926  dfima2  5024  dfima3  5025  imadmrn  5032  imai  5038  args  5051  mptpreima  5176  dfiota2  5233  cbviota  5237  sb8iota  5239  dffv4g  5573  dfimafn2  5628  fnasrn  5758  fnasrng  5760  elabrex  5826  elabrexg  5827  abrexco  5828  dfoprab2  5992  cbvoprab2  6018  dmoprab  6026  rnoprab  6028  rnoprab2  6029  fnrnov  6092  abrexex2g  6205  abrexex2  6209  abexssex  6210  abexex  6211  oprabrexex2  6215  dfopab2  6275  cnvoprab  6320  tfr1onlemaccex  6434  tfrcllemaccex  6447  tfrcldm  6449  frec0g  6483  frecsuc  6493  snec  6683  pmex  6740  dfixp  6787  cbvixp  6802  caucvgprprlemmu  7808  caucvgsr  7915  pitonnlem1  7958  mertenslem2  11847  4sqlemafi  12718  dfrhm2  13916  toponsspwpwg  14494  tgval2  14523  2lgslem1b  15566  if0ab  15745  bdcuni  15816  bj-dfom  15873