Theorem abbii 2312

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189

This theorem is referenced by:  rabswap  2676  rabbiia  2748  rabab  2784  csb2  3086  cbvcsbw  3088  cbvcsb  3089  csbid  3092  csbco  3094  csbcow  3095  cbvreucsf  3149  unrab  3434  inrab  3435  inrab2  3436  difrab  3437  rabun2  3442  dfnul3  3453  rab0  3479  tprot  3715  pw0  3769  dfuni2  3841  unipr  3853  dfint2  3876  int0  3888  dfiunv2  3952  cbviun  3953  cbviin  3954  iunrab  3964  iunid  3972  viin  3976  cbvopab  4104  cbvopab1  4106  cbvopab2  4107  cbvopab1s  4108  cbvopab2v  4110  unopab  4112  iunopab  4316  abnex  4482  uniuni  4486  ruv  4586  rabxp  4700  dfdm3  4853  dfrn2  4854  dfrn3  4855  dfdm4  4858  dfdmf  4859  dmun  4873  dmopab  4877  dmopabss  4878  dmopab3  4879  dfrnf  4907  rnopab  4913  rnmpt  4914  dfima2  5011  dfima3  5012  imadmrn  5019  imai  5025  args  5038  mptpreima  5163  dfiota2  5220  cbviota  5224  sb8iota  5226  dffv4g  5555  dfimafn2  5610  fnasrn  5740  fnasrng  5742  elabrex  5804  elabrexg  5805  abrexco  5806  dfoprab2  5969  cbvoprab2  5995  dmoprab  6003  rnoprab  6005  rnoprab2  6006  fnrnov  6069  abrexex2g  6177  abrexex2  6181  abexssex  6182  abexex  6183  oprabrexex2  6187  dfopab2  6247  cnvoprab  6292  tfr1onlemaccex  6406  tfrcllemaccex  6419  tfrcldm  6421  frec0g  6455  frecsuc  6465  snec  6655  pmex  6712  dfixp  6759  cbvixp  6774  caucvgprprlemmu  7762  caucvgsr  7869  pitonnlem1  7912  mertenslem2  11701  4sqlemafi  12564  dfrhm2  13710  toponsspwpwg  14258  tgval2  14287  2lgslem1b  15330  if0ab  15451  bdcuni  15522  bj-dfom  15579