Theorem abbii 2286

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

Syntax hints:   <-> wb 104   = wceq 1348   {cab 2156

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163

This theorem is referenced by:  rabswap  2648  rabbiia  2715  rabab  2751  csb2  3051  cbvcsbw  3053  cbvcsb  3054  csbid  3057  csbco  3059  csbcow  3060  cbvreucsf  3113  unrab  3398  inrab  3399  inrab2  3400  difrab  3401  rabun2  3406  dfnul3  3417  rab0  3443  tprot  3676  pw0  3727  dfuni2  3798  unipr  3810  dfint2  3833  int0  3845  dfiunv2  3909  cbviun  3910  cbviin  3911  iunrab  3920  iunid  3928  viin  3932  cbvopab  4060  cbvopab1  4062  cbvopab2  4063  cbvopab1s  4064  cbvopab2v  4066  unopab  4068  iunopab  4266  abnex  4432  uniuni  4436  ruv  4534  rabxp  4648  dfdm3  4798  dfrn2  4799  dfrn3  4800  dfdm4  4803  dfdmf  4804  dmun  4818  dmopab  4822  dmopabss  4823  dmopab3  4824  dfrnf  4852  rnopab  4858  rnmpt  4859  dfima2  4955  dfima3  4956  imadmrn  4963  imai  4967  args  4980  mptpreima  5104  dfiota2  5161  cbviota  5165  sb8iota  5167  dffv4g  5493  dfimafn2  5546  fnasrn  5674  fnasrng  5676  elabrex  5737  abrexco  5738  dfoprab2  5900  cbvoprab2  5926  dmoprab  5934  rnoprab  5936  rnoprab2  5937  fnrnov  5998  abrexex2g  6099  abrexex2  6103  abexssex  6104  abexex  6105  oprabrexex2  6109  dfopab2  6168  cnvoprab  6213  tfr1onlemaccex  6327  tfrcllemaccex  6340  tfrcldm  6342  frec0g  6376  frecsuc  6386  snec  6574  pmex  6631  dfixp  6678  cbvixp  6693  caucvgprprlemmu  7657  caucvgsr  7764  pitonnlem1  7807  mertenslem2  11499  toponsspwpwg  12814  tgval2  12845  if0ab  13840  bdcuni  13911  bj-dfom  13968