Theorem abbii 2291

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

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

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168

This theorem is referenced by:  rabswap  2653  rabbiia  2720  rabab  2756  csb2  3057  cbvcsbw  3059  cbvcsb  3060  csbid  3063  csbco  3065  csbcow  3066  cbvreucsf  3119  unrab  3404  inrab  3405  inrab2  3406  difrab  3407  rabun2  3412  dfnul3  3423  rab0  3449  tprot  3682  pw0  3736  dfuni2  3807  unipr  3819  dfint2  3842  int0  3854  dfiunv2  3918  cbviun  3919  cbviin  3920  iunrab  3929  iunid  3937  viin  3941  cbvopab  4069  cbvopab1  4071  cbvopab2  4072  cbvopab1s  4073  cbvopab2v  4075  unopab  4077  iunopab  4275  abnex  4441  uniuni  4445  ruv  4543  rabxp  4657  dfdm3  4807  dfrn2  4808  dfrn3  4809  dfdm4  4812  dfdmf  4813  dmun  4827  dmopab  4831  dmopabss  4832  dmopab3  4833  dfrnf  4861  rnopab  4867  rnmpt  4868  dfima2  4965  dfima3  4966  imadmrn  4973  imai  4977  args  4990  mptpreima  5114  dfiota2  5171  cbviota  5175  sb8iota  5177  dffv4g  5504  dfimafn2  5557  fnasrn  5686  fnasrng  5688  elabrex  5749  abrexco  5750  dfoprab2  5912  cbvoprab2  5938  dmoprab  5946  rnoprab  5948  rnoprab2  5949  fnrnov  6010  abrexex2g  6111  abrexex2  6115  abexssex  6116  abexex  6117  oprabrexex2  6121  dfopab2  6180  cnvoprab  6225  tfr1onlemaccex  6339  tfrcllemaccex  6352  tfrcldm  6354  frec0g  6388  frecsuc  6398  snec  6586  pmex  6643  dfixp  6690  cbvixp  6705  caucvgprprlemmu  7669  caucvgsr  7776  pitonnlem1  7819  mertenslem2  11512  toponsspwpwg  13100  tgval2  13131  if0ab  14126  bdcuni  14197  bj-dfom  14254