Theorem abbii 2198

Description: Equivalent wff's yield equal class abstractions (inference rule). (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 2196	. 2 |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
2		abbii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpgbi 1382	1 |- { x | ph } = { x | ps }

Syntax hints:   <-> wb 103   = wceq 1285   {cab 2069

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076

This theorem is referenced by:  rabswap  2538  rabbiia  2597  rabab  2631  csb2  2921  cbvcsb  2923  csbid  2926  csbco  2928  cbvreucsf  2977  unrab  3253  inrab  3254  inrab2  3255  difrab  3256  rabun2  3261  dfnul3  3272  rab0  3294  tprot  3509  pw0  3558  dfuni2  3629  unipr  3641  dfint2  3664  int0  3676  dfiunv2  3740  cbviun  3741  cbviin  3742  iunrab  3751  iunid  3759  viin  3763  cbvopab  3875  cbvopab1  3877  cbvopab2  3878  cbvopab1s  3879  cbvopab2v  3881  unopab  3883  iunopab  4072  uniuni  4237  ruv  4329  rabxp  4436  dfdm3  4581  dfrn2  4582  dfrn3  4583  dfdm4  4586  dfdmf  4587  dmun  4601  dmopab  4605  dmopabss  4606  dmopab3  4607  dfrnf  4634  rnopab  4640  rnmpt  4641  dfima2  4731  dfima3  4732  imadmrn  4739  imai  4743  args  4756  mptpreima  4878  dfiota2  4935  cbviota  4939  sb8iota  4941  dffv4g  5250  dfimafn2  5299  fnasrn  5417  fnasrng  5419  elabrex  5477  abrexco  5478  dfoprab2  5631  cbvoprab2  5656  dmoprab  5664  rnoprab  5666  rnoprab2  5667  fnrnov  5725  abrexex2g  5826  abrexex2  5830  abexssex  5831  abexex  5832  oprabrexex2  5836  dfopab2  5894  cnvoprab  5934  tfr1onlemaccex  6045  tfrcllemaccex  6058  tfrcldm  6060  frec0g  6094  frecsuc  6104  snec  6283  pmex  6340  caucvgprprlemmu  7157  caucvgsr  7250  pitonnlem1  7285  bdcuni  11110  bj-dfom  11171