Theorem abbii 2345

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

Syntax hints:   <-> wb 105   = wceq 1395   {cab 2215

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222

This theorem is referenced by:  rabswap  2710  rabbiia  2784  rabab  2821  csb2  3126  cbvcsbw  3128  cbvcsb  3129  csbid  3132  csbco  3134  csbcow  3135  cbvreucsf  3189  unrab  3475  inrab  3476  inrab2  3477  difrab  3478  rabun2  3483  dfnul3  3494  rab0  3520  tprot  3759  pw0  3815  dfuni2  3890  unipr  3902  dfint2  3925  int0  3937  dfiunv2  4001  cbviun  4002  cbviin  4003  iunrab  4013  iunid  4021  viin  4025  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab2v  4161  unopab  4163  iunopab  4370  abnex  4538  uniuni  4542  ruv  4642  rabxp  4756  dfdm3  4909  dfrn2  4910  dfrn3  4911  dfdm4  4915  dfdmf  4916  dmun  4930  dmopab  4934  dmopabss  4935  dmopab3  4936  dfrnf  4965  rnopab  4971  rnmpt  4972  dfima2  5070  dfima3  5071  imadmrn  5078  imai  5084  args  5097  mptpreima  5222  dfiota2  5279  cbviota  5283  cbviotavw  5284  sb8iota  5286  dffv4g  5624  dfimafn2  5683  fnasrn  5813  fnasrng  5815  elabrex  5881  elabrexg  5882  abrexco  5883  dfoprab2  6051  cbvoprab2  6077  dmoprab  6085  rnoprab  6087  rnoprab2  6088  fnrnov  6151  abrexex2g  6265  abrexex2  6269  abexssex  6270  abexex  6271  oprabrexex2  6275  dfopab2  6335  cnvoprab  6380  tfr1onlemaccex  6494  tfrcllemaccex  6507  tfrcldm  6509  frec0g  6543  frecsuc  6553  snec  6743  pmex  6800  dfixp  6847  cbvixp  6862  caucvgprprlemmu  7882  caucvgsr  7989  pitonnlem1  8032  mertenslem2  12047  4sqlemafi  12918  dfrhm2  14118  toponsspwpwg  14696  tgval2  14725  2lgslem1b  15768  if0ab  16169  bdcuni  16239  bj-dfom  16296