Theorem abbii 2350

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 2348	. 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 2220

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 2216

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

This theorem is referenced by:  rabswap  2725  rabbiia  2801  rabab  2837  csb2  3143  cbvcsbw  3145  cbvcsb  3146  csbid  3149  csbco  3151  csbcow  3152  cbvreucsf  3206  unrab  3496  inrab  3497  inrab2  3498  difrab  3499  rabun2  3504  dfnul3  3515  rab0  3541  rabsnifsb  3762  tprot  3789  pw0  3846  dfuni2  3921  unipr  3933  dfint2  3956  int0  3968  dfiunv2  4032  cbviun  4033  cbviin  4034  iunrab  4044  iunid  4052  viin  4056  cbvopab  4186  cbvopab1  4188  cbvopab2  4189  cbvopab1s  4190  cbvopab2v  4192  unopab  4194  iunopab  4405  abnex  4573  uniuni  4577  ruv  4677  rabxp  4792  dfdm3  4947  dfrn2  4948  dfrn3  4949  dfdm4  4953  dfdmf  4954  dmun  4968  dmopab  4972  dmopabss  4973  dmopab3  4974  dfrnf  5003  rnopab  5009  rnmpt  5010  dfima2  5108  dfima3  5109  imadmrn  5116  imai  5123  args  5136  mptpreima  5261  dfiota2  5318  cbviota  5322  cbviotavw  5323  sb8iota  5325  dffv4g  5672  dfimafn2  5731  fnasrn  5861  fnasrng  5863  dfimafnf  5928  elabrex  5936  elabrexg  5937  abrexco  5938  dfoprab2  6108  cbvoprab2  6134  dmoprab  6142  rnoprab  6144  rnoprab2  6145  fnrnov  6208  abrexex2g  6322  abrexex2  6326  abexssex  6327  abexex  6328  oprabrexex2  6336  dfopab2  6396  cnvoprab  6443  cnvimadfsn  6458  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfrcldm  6607  frec0g  6641  frecsuc  6651  snec  6843  pmex  6900  dfixp  6948  cbvixp  6963  caucvgprprlemmu  8026  caucvgsr  8133  pitonnlem1  8176  mertenslem2  12247  4sqlemafi  13118  dfrhm2  14399  toponsspwpwg  15013  tgval2  15042  2lgslem1b  16088  bdcuni  16772  bj-dfom  16829