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  3435  inrab  3436  inrab2  3437  difrab  3438  rabun2  3443  dfnul3  3454  rab0  3480  tprot  3716  pw0  3770  dfuni2  3842  unipr  3854  dfint2  3877  int0  3889  dfiunv2  3953  cbviun  3954  cbviin  3955  iunrab  3965  iunid  3973  viin  3977  cbvopab  4105  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  cbvopab2v  4111  unopab  4113  iunopab  4317  abnex  4483  uniuni  4487  ruv  4587  rabxp  4701  dfdm3  4854  dfrn2  4855  dfrn3  4856  dfdm4  4859  dfdmf  4860  dmun  4874  dmopab  4878  dmopabss  4879  dmopab3  4880  dfrnf  4908  rnopab  4914  rnmpt  4915  dfima2  5012  dfima3  5013  imadmrn  5020  imai  5026  args  5039  mptpreima  5164  dfiota2  5221  cbviota  5225  sb8iota  5227  dffv4g  5556  dfimafn2  5611  fnasrn  5741  fnasrng  5743  elabrex  5805  elabrexg  5806  abrexco  5807  dfoprab2  5970  cbvoprab2  5996  dmoprab  6004  rnoprab  6006  rnoprab2  6007  fnrnov  6070  abrexex2g  6178  abrexex2  6182  abexssex  6183  abexex  6184  oprabrexex2  6188  dfopab2  6248  cnvoprab  6293  tfr1onlemaccex  6407  tfrcllemaccex  6420  tfrcldm  6422  frec0g  6456  frecsuc  6466  snec  6656  pmex  6713  dfixp  6760  cbvixp  6775  caucvgprprlemmu  7764  caucvgsr  7871  pitonnlem1  7914  mertenslem2  11703  4sqlemafi  12574  dfrhm2  13720  toponsspwpwg  14268  tgval2  14297  2lgslem1b  15340  if0ab  15461  bdcuni  15532  bj-dfom  15589