Theorem abbii 2204

Description: Equivalent wff's yield equal class abstractions (inference form). (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 2202	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpgbi 1387	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 104   = wceq 1290  {cab 2075

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082

This theorem is referenced by:  rabswap  2546  rabbiia  2605  rabab  2641  csb2  2936  cbvcsb  2938  csbid  2941  csbco  2943  cbvreucsf  2993  unrab  3271  inrab  3272  inrab2  3273  difrab  3274  rabun2  3279  dfnul3  3290  rab0  3315  tprot  3539  pw0  3590  dfuni2  3661  unipr  3673  dfint2  3696  int0  3708  dfiunv2  3772  cbviun  3773  cbviin  3774  iunrab  3783  iunid  3791  viin  3795  cbvopab  3915  cbvopab1  3917  cbvopab2  3918  cbvopab1s  3919  cbvopab2v  3921  unopab  3923  iunopab  4117  abnex  4282  uniuni  4286  ruv  4379  rabxp  4487  dfdm3  4636  dfrn2  4637  dfrn3  4638  dfdm4  4641  dfdmf  4642  dmun  4656  dmopab  4660  dmopabss  4661  dmopab3  4662  dfrnf  4689  rnopab  4695  rnmpt  4696  dfima2  4789  dfima3  4790  imadmrn  4797  imai  4801  args  4814  mptpreima  4937  dfiota2  4994  cbviota  4998  sb8iota  5000  dffv4g  5315  dfimafn2  5367  fnasrn  5489  fnasrng  5491  elabrex  5551  abrexco  5552  dfoprab2  5710  cbvoprab2  5735  dmoprab  5743  rnoprab  5745  rnoprab2  5746  fnrnov  5804  abrexex2g  5905  abrexex2  5909  abexssex  5910  abexex  5911  oprabrexex2  5915  dfopab2  5973  cnvoprab  6013  tfr1onlemaccex  6127  tfrcllemaccex  6140  tfrcldm  6142  frec0g  6176  frecsuc  6186  snec  6367  pmex  6424  dfixp  6471  cbvixp  6486  caucvgprprlemmu  7308  caucvgsr  7401  pitonnlem1  7436  mertenslem2  10984  toponsspwpwg  11774  tgval2  11805  bdcuni  12033  bj-dfom  12094