Theorem abbii 2150

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 2148	. 2 ⊢ (∀x(φ ↔ ψ) ↔ {x ∣ φ} = {x ∣ ψ})
2		abbii.1	. 2 ⊢ (φ ↔ ψ)
3	1, 2	mpgbi 1338	1 ⊢ {x ∣ φ} = {x ∣ ψ}

Syntax hints:   ↔ wb 98   = wceq 1242  {cab 2023

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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030

This theorem is referenced by:  rabswap  2482  rabbiia  2541  rabab  2569  csb2  2848  cbvcsb  2850  csbid  2853  csbco  2855  cbvreucsf  2904  unrab  3202  inrab  3203  inrab2  3204  difrab  3205  rabun2  3210  dfnul3  3221  rab0  3240  tprot  3454  pw0  3502  dfuni2  3573  unipr  3585  dfint2  3608  int0  3620  dfiunv2  3684  cbviun  3685  cbviin  3686  iunrab  3695  iunid  3703  viin  3707  cbvopab  3819  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  cbvopab2v  3825  unopab  3827  iunopab  4009  uniuni  4149  ruv  4228  rabxp  4323  dfdm3  4465  dfrn2  4466  dfrn3  4467  dfdm4  4470  dfdmf  4471  dmun  4485  dmopab  4489  dmopabss  4490  dmopab3  4491  dfrnf  4518  rnopab  4524  rnmpt  4525  dfima2  4613  dfima3  4614  imadmrn  4621  imai  4624  args  4637  mptpreima  4757  dfiota2  4811  cbviota  4815  sb8iota  4817  dffv4g  5118  dfimafn2  5166  fnasrn  5284  fnasrng  5286  elabrex  5340  abrexco  5341  dfoprab2  5494  cbvoprab2  5519  dmoprab  5527  rnoprab  5529  rnoprab2  5530  fnrnov  5588  abrexex2g  5689  abrexex2  5693  abexssex  5694  abexex  5695  oprabrexex2  5699  dfopab2  5757  frec0g  5922  frecsuc  5930  snec  6103  pitonnlem1  6741  bdcuni  9331  bj-dfom  9392