Theorem abbii 2131

Description: Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
abbii.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
abbii	⊢ {x ∣ φ} = {x ∣ ψ}

Proof of Theorem abbii

Step	Hyp	Ref	Expression
1		abbi 2129	. 2 ⊢ (∀x(φ ↔ ψ) ↔ {x ∣ φ} = {x ∣ ψ})
2		abbii.1	. 2 ⊢ (φ ↔ ψ)
3	1, 2	mpgbi 1317	1 ⊢ {x ∣ φ} = {x ∣ ψ}

Syntax hints:   ↔ wb 98   = wceq 1226  {cab 2004

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-11 1374  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011

This theorem is referenced by:  rabswap  2462  rabbiia  2521  rabab  2548  csb2  2827  cbvcsb  2829  csbid  2832  csbco  2834  cbvreucsf  2883  unrab  3181  inrab  3182  inrab2  3183  difrab  3184  rabun2  3189  dfnul3  3200  rab0  3219  tprot  3433  pw0  3481  dfuni2  3552  unipr  3564  dfint2  3587  int0  3599  dfiunv2  3663  cbviun  3664  cbviin  3665  iunrab  3674  iunid  3682  viin  3686  cbvopab  3798  cbvopab1  3800  cbvopab2  3801  cbvopab1s  3802  cbvopab2v  3804  unopab  3806  iunopab  3988  uniuni  4129  ruv  4208  rabxp  4303  dfdm3  4445  dfrn2  4446  dfrn3  4447  dfdm4  4450  dfdmf  4451  dmun  4465  dmopab  4469  dmopabss  4470  dmopab3  4471  dfrnf  4498  rnopab  4504  rnmpt  4505  dfima2  4593  dfima3  4594  imadmrn  4601  imai  4604  args  4617  mptpreima  4737  dfiota2  4791  cbviota  4795  sb8iota  4797  dffv4g  5096  dfimafn2  5144  fnasrn  5262  fnasrng  5264  elabrex  5318  abrexco  5319  dfoprab2  5471  cbvoprab2  5496  dmoprab  5504  rnoprab  5506  rnoprab2  5507  fnrnov  5565  abrexex2g  5666  abrexex2  5670  abexssex  5671  abexex  5672  oprabrexex2  5676  dfopab2  5734  frec0g  5898  frecsuc  5903  snec  6074  bdcuni  7242  bj-dfom  7294