Theorem abbii 2153

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	⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Proof of Theorem abbii

Step	Hyp	Ref	Expression
1		abbi 2151	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpgbi 1341	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 98   = wceq 1243  {cab 2026

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 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033

This theorem is referenced by:  rabswap  2488  rabbiia  2547  rabab  2575  csb2  2854  cbvcsb  2856  csbid  2859  csbco  2861  cbvreucsf  2910  unrab  3208  inrab  3209  inrab2  3210  difrab  3211  rabun2  3216  dfnul3  3227  rab0  3246  tprot  3463  pw0  3511  dfuni2  3582  unipr  3594  dfint2  3617  int0  3629  dfiunv2  3693  cbviun  3694  cbviin  3695  iunrab  3704  iunid  3712  viin  3716  cbvopab  3828  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  cbvopab2v  3834  unopab  3836  iunopab  4018  uniuni  4183  ruv  4274  rabxp  4380  dfdm3  4522  dfrn2  4523  dfrn3  4524  dfdm4  4527  dfdmf  4528  dmun  4542  dmopab  4546  dmopabss  4547  dmopab3  4548  dfrnf  4575  rnopab  4581  rnmpt  4582  dfima2  4670  dfima3  4671  imadmrn  4678  imai  4681  args  4694  mptpreima  4814  dfiota2  4868  cbviota  4872  sb8iota  4874  dffv4g  5175  dfimafn2  5223  fnasrn  5341  fnasrng  5343  elabrex  5397  abrexco  5398  dfoprab2  5552  cbvoprab2  5577  dmoprab  5585  rnoprab  5587  rnoprab2  5588  fnrnov  5646  abrexex2g  5747  abrexex2  5751  abexssex  5752  abexex  5753  oprabrexex2  5757  dfopab2  5815  frec0g  5983  frecsuc  5991  snec  6167  caucvgprprlemmu  6793  caucvgsr  6886  pitonnlem1  6921  bdcuni  9996  bj-dfom  10057