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  5558  dfimafn2  5613  fnasrn  5743  fnasrng  5745  elabrex  5807  elabrexg  5808  abrexco  5809  dfoprab2  5973  cbvoprab2  5999  dmoprab  6007  rnoprab  6009  rnoprab2  6010  fnrnov  6073  abrexex2g  6186  abrexex2  6190  abexssex  6191  abexex  6192  oprabrexex2  6196  dfopab2  6256  cnvoprab  6301  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfrcldm  6430  frec0g  6464  frecsuc  6474  snec  6664  pmex  6721  dfixp  6768  cbvixp  6783  caucvgprprlemmu  7779  caucvgsr  7886  pitonnlem1  7929  mertenslem2  11718  4sqlemafi  12589  dfrhm2  13786  toponsspwpwg  14342  tgval2  14371  2lgslem1b  15414  if0ab  15535  bdcuni  15606  bj-dfom  15663