Theorem abbii 2348

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

Syntax hints:   <-> wb 105   = wceq 1398   {cab 2218

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225

This theorem is referenced by:  rabswap  2723  rabbiia  2799  rabab  2835  csb2  3140  cbvcsbw  3142  cbvcsb  3143  csbid  3146  csbco  3148  csbcow  3149  cbvreucsf  3203  unrab  3492  inrab  3493  inrab2  3494  difrab  3495  rabun2  3500  dfnul3  3511  rab0  3537  rabsnifsb  3757  tprot  3784  pw0  3841  dfuni2  3916  unipr  3928  dfint2  3951  int0  3963  dfiunv2  4027  cbviun  4028  cbviin  4029  iunrab  4039  iunid  4047  viin  4051  cbvopab  4181  cbvopab1  4183  cbvopab2  4184  cbvopab1s  4185  cbvopab2v  4187  unopab  4189  iunopab  4400  abnex  4568  uniuni  4572  ruv  4672  rabxp  4787  dfdm3  4942  dfrn2  4943  dfrn3  4944  dfdm4  4948  dfdmf  4949  dmun  4963  dmopab  4967  dmopabss  4968  dmopab3  4969  dfrnf  4998  rnopab  5004  rnmpt  5005  dfima2  5103  dfima3  5104  imadmrn  5111  imai  5118  args  5131  mptpreima  5256  dfiota2  5313  cbviota  5317  cbviotavw  5318  sb8iota  5320  dffv4g  5667  dfimafn2  5726  fnasrn  5856  fnasrng  5858  elabrex  5930  elabrexg  5931  abrexco  5932  dfoprab2  6100  cbvoprab2  6126  dmoprab  6134  rnoprab  6136  rnoprab2  6137  fnrnov  6200  abrexex2g  6313  abrexex2  6317  abexssex  6318  abexex  6319  oprabrexex2  6323  dfopab2  6383  cnvoprab  6430  cnvimadfsn  6445  tfr1onlemaccex  6579  tfrcllemaccex  6592  tfrcldm  6594  frec0g  6628  frecsuc  6638  snec  6830  pmex  6887  dfixp  6935  cbvixp  6950  caucvgprprlemmu  8010  caucvgsr  8117  pitonnlem1  8160  mertenslem2  12222  4sqlemafi  13093  dfrhm2  14299  toponsspwpwg  14887  tgval2  14916  2lgslem1b  15962  bdcuni  16646  bj-dfom  16703