Theorem abbii 2305

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

Syntax hints:   <-> wb 105   = wceq 1364   {cab 2175

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182

This theorem is referenced by:  rabswap  2669  rabbiia  2737  rabab  2773  csb2  3074  cbvcsbw  3076  cbvcsb  3077  csbid  3080  csbco  3082  csbcow  3083  cbvreucsf  3136  unrab  3421  inrab  3422  inrab2  3423  difrab  3424  rabun2  3429  dfnul3  3440  rab0  3466  tprot  3700  pw0  3754  dfuni2  3826  unipr  3838  dfint2  3861  int0  3873  dfiunv2  3937  cbviun  3938  cbviin  3939  iunrab  3949  iunid  3957  viin  3961  cbvopab  4089  cbvopab1  4091  cbvopab2  4092  cbvopab1s  4093  cbvopab2v  4095  unopab  4097  iunopab  4299  abnex  4465  uniuni  4469  ruv  4567  rabxp  4681  dfdm3  4832  dfrn2  4833  dfrn3  4834  dfdm4  4837  dfdmf  4838  dmun  4852  dmopab  4856  dmopabss  4857  dmopab3  4858  dfrnf  4886  rnopab  4892  rnmpt  4893  dfima2  4990  dfima3  4991  imadmrn  4998  imai  5002  args  5015  mptpreima  5140  dfiota2  5197  cbviota  5201  sb8iota  5203  dffv4g  5531  dfimafn2  5586  fnasrn  5715  fnasrng  5717  elabrex  5779  elabrexg  5780  abrexco  5781  dfoprab2  5943  cbvoprab2  5969  dmoprab  5977  rnoprab  5979  rnoprab2  5980  fnrnov  6042  abrexex2g  6145  abrexex2  6149  abexssex  6150  abexex  6151  oprabrexex2  6155  dfopab2  6214  cnvoprab  6259  tfr1onlemaccex  6373  tfrcllemaccex  6386  tfrcldm  6388  frec0g  6422  frecsuc  6432  snec  6622  pmex  6679  dfixp  6726  cbvixp  6741  caucvgprprlemmu  7724  caucvgsr  7831  pitonnlem1  7874  mertenslem2  11576  4sqlemafi  12427  dfrhm2  13504  toponsspwpwg  13982  tgval2  14011  if0ab  15018  bdcuni  15089  bj-dfom  15146