Theorem abbii 2321

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

Syntax hints:   <-> wb 105   = wceq 1373   {cab 2191

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198

This theorem is referenced by:  rabswap  2685  rabbiia  2757  rabab  2793  csb2  3095  cbvcsbw  3097  cbvcsb  3098  csbid  3101  csbco  3103  csbcow  3104  cbvreucsf  3158  unrab  3444  inrab  3445  inrab2  3446  difrab  3447  rabun2  3452  dfnul3  3463  rab0  3489  tprot  3726  pw0  3780  dfuni2  3852  unipr  3864  dfint2  3887  int0  3899  dfiunv2  3963  cbviun  3964  cbviin  3965  iunrab  3975  iunid  3983  viin  3987  cbvopab  4116  cbvopab1  4118  cbvopab2  4119  cbvopab1s  4120  cbvopab2v  4122  unopab  4124  iunopab  4329  abnex  4495  uniuni  4499  ruv  4599  rabxp  4713  dfdm3  4866  dfrn2  4867  dfrn3  4868  dfdm4  4871  dfdmf  4872  dmun  4886  dmopab  4890  dmopabss  4891  dmopab3  4892  dfrnf  4920  rnopab  4926  rnmpt  4927  dfima2  5025  dfima3  5026  imadmrn  5033  imai  5039  args  5052  mptpreima  5177  dfiota2  5234  cbviota  5238  sb8iota  5240  dffv4g  5575  dfimafn2  5630  fnasrn  5760  fnasrng  5762  elabrex  5828  elabrexg  5829  abrexco  5830  dfoprab2  5994  cbvoprab2  6020  dmoprab  6028  rnoprab  6030  rnoprab2  6031  fnrnov  6094  abrexex2g  6207  abrexex2  6211  abexssex  6212  abexex  6213  oprabrexex2  6217  dfopab2  6277  cnvoprab  6322  tfr1onlemaccex  6436  tfrcllemaccex  6449  tfrcldm  6451  frec0g  6485  frecsuc  6495  snec  6685  pmex  6742  dfixp  6789  cbvixp  6804  caucvgprprlemmu  7810  caucvgsr  7917  pitonnlem1  7960  mertenslem2  11880  4sqlemafi  12751  dfrhm2  13949  toponsspwpwg  14527  tgval2  14556  2lgslem1b  15599  if0ab  15778  bdcuni  15849  bj-dfom  15906