Theorem abbii 2293

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

Syntax hints:   <-> wb 105   = wceq 1353   {cab 2163

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170

This theorem is referenced by:  rabswap  2656  rabbiia  2723  rabab  2759  csb2  3060  cbvcsbw  3062  cbvcsb  3063  csbid  3066  csbco  3068  csbcow  3069  cbvreucsf  3122  unrab  3407  inrab  3408  inrab2  3409  difrab  3410  rabun2  3415  dfnul3  3426  rab0  3452  tprot  3686  pw0  3740  dfuni2  3812  unipr  3824  dfint2  3847  int0  3859  dfiunv2  3923  cbviun  3924  cbviin  3925  iunrab  3935  iunid  3943  viin  3947  cbvopab  4075  cbvopab1  4077  cbvopab2  4078  cbvopab1s  4079  cbvopab2v  4081  unopab  4083  iunopab  4282  abnex  4448  uniuni  4452  ruv  4550  rabxp  4664  dfdm3  4815  dfrn2  4816  dfrn3  4817  dfdm4  4820  dfdmf  4821  dmun  4835  dmopab  4839  dmopabss  4840  dmopab3  4841  dfrnf  4869  rnopab  4875  rnmpt  4876  dfima2  4973  dfima3  4974  imadmrn  4981  imai  4985  args  4998  mptpreima  5123  dfiota2  5180  cbviota  5184  sb8iota  5186  dffv4g  5513  dfimafn2  5566  fnasrn  5695  fnasrng  5697  elabrex  5759  abrexco  5760  dfoprab2  5922  cbvoprab2  5948  dmoprab  5956  rnoprab  5958  rnoprab2  5959  fnrnov  6020  abrexex2g  6121  abrexex2  6125  abexssex  6126  abexex  6127  oprabrexex2  6131  dfopab2  6190  cnvoprab  6235  tfr1onlemaccex  6349  tfrcllemaccex  6362  tfrcldm  6364  frec0g  6398  frecsuc  6408  snec  6596  pmex  6653  dfixp  6700  cbvixp  6715  caucvgprprlemmu  7694  caucvgsr  7801  pitonnlem1  7844  mertenslem2  11544  toponsspwpwg  13525  tgval2  13554  if0ab  14560  bdcuni  14631  bj-dfom  14688