Theorem abbii 2354

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

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402   {cab 2224

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231

This theorem is used by:  rabswap  2731  rabbiia  2807  rabab  2843  csb2  3149  cbvcsbw  3151  cbvcsb  3152  csbid  3155  csbco  3157  csbcow  3158  cbvreucsf  3212  unrab  3504  inrab  3505  inrab2  3506  difrab  3507  rabun2  3512  dfnul4  3522  dfnul2  3523  dfnul3  3524  rab0  3551  rabsnifsb  3777  tprot  3804  pw0  3862  dfuni2  3937  unipr  3949  dfint2  3972  int0  3984  dfiunv2  4048  cbviun  4049  cbviin  4050  iunrab  4060  iunid  4068  viin  4072  cbvopab  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab2v  4208  unopab  4210  iunopab  4424  abnex  4593  uniuni  4597  ruv  4697  rabxp  4812  dfdm3  4967  dfrn2  4968  dfrn3  4969  dfdm4  4973  dfdmf  4974  dmun  4988  dmopab  4992  dmopabss  4993  dmopab3  4994  dfrnf  5023  rnopab  5029  rnmpt  5030  dfima2  5128  dfima3  5129  imadmrn  5136  imai  5143  args  5156  mptpreima  5281  dfiota2  5338  cbviota  5342  cbviotavw  5343  sb8iota  5345  dffv4g  5692  dfimafn2  5752  fnasrn  5887  fnasrng  5889  dfimafnf  5955  elabrex  5963  elabrexg  5964  abrexco  5965  dfoprab2  6135  cbvoprab2  6161  dmoprab  6169  rnoprab  6171  rnoprab2  6172  fnrnov  6235  abrexex2g  6349  abrexex2  6353  abexssex  6354  abexex  6355  oprabrexex2  6363  dfopab2  6423  cnvoprab  6470  cnvimadfsn  6485  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcldm  6634  frec0g  6668  frecsuc  6678  snec  6870  pmex  6927  fset0  6949  f1setexg  6951  dfixp  6982  cbvixp  6997  caucvgprprlemmu  8062  caucvgsr  8169  pitonnlem1  8212  hashf1lem2  11286  mertenslem2  12303  4sqlemafi  13174  dfrhm2  14461  toponsspwpwg  15123  tgval2  15152  2lgslem1b  16208  bdcuni  16902  bj-dfom  16959