Theorem abbii 2203

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

Syntax hints:   <-> wb 103   = wceq 1289   {cab 2074

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081

This theorem is referenced by:  rabswap  2545  rabbiia  2604  rabab  2640  csb2  2933  cbvcsb  2935  csbid  2938  csbco  2940  cbvreucsf  2990  unrab  3268  inrab  3269  inrab2  3270  difrab  3271  rabun2  3276  dfnul3  3287  rab0  3309  tprot  3530  pw0  3579  dfuni2  3650  unipr  3662  dfint2  3685  int0  3697  dfiunv2  3761  cbviun  3762  cbviin  3763  iunrab  3772  iunid  3780  viin  3784  cbvopab  3901  cbvopab1  3903  cbvopab2  3904  cbvopab1s  3905  cbvopab2v  3907  unopab  3909  iunopab  4099  uniuni  4264  ruv  4356  rabxp  4463  dfdm3  4611  dfrn2  4612  dfrn3  4613  dfdm4  4616  dfdmf  4617  dmun  4631  dmopab  4635  dmopabss  4636  dmopab3  4637  dfrnf  4664  rnopab  4670  rnmpt  4671  dfima2  4763  dfima3  4764  imadmrn  4771  imai  4775  args  4788  mptpreima  4911  dfiota2  4968  cbviota  4972  sb8iota  4974  dffv4g  5286  dfimafn2  5338  fnasrn  5459  fnasrng  5461  elabrex  5519  abrexco  5520  dfoprab2  5678  cbvoprab2  5703  dmoprab  5711  rnoprab  5713  rnoprab2  5714  fnrnov  5772  abrexex2g  5873  abrexex2  5877  abexssex  5878  abexex  5879  oprabrexex2  5883  dfopab2  5941  cnvoprab  5981  tfr1onlemaccex  6095  tfrcllemaccex  6108  tfrcldm  6110  frec0g  6144  frecsuc  6154  snec  6333  pmex  6390  caucvgprprlemmu  7233  caucvgsr  7326  pitonnlem1  7361  bdcuni  11413  bj-dfom  11474