Theorem abbii 2309

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 2307	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpgbi 1463	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 105   = wceq 1364  {cab 2179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186

This theorem is referenced by:  rabswap  2673  rabbiia  2745  rabab  2781  csb2  3083  cbvcsbw  3085  cbvcsb  3086  csbid  3089  csbco  3091  csbcow  3092  cbvreucsf  3146  unrab  3431  inrab  3432  inrab2  3433  difrab  3434  rabun2  3439  dfnul3  3450  rab0  3476  tprot  3712  pw0  3766  dfuni2  3838  unipr  3850  dfint2  3873  int0  3885  dfiunv2  3949  cbviun  3950  cbviin  3951  iunrab  3961  iunid  3969  viin  3973  cbvopab  4101  cbvopab1  4103  cbvopab2  4104  cbvopab1s  4105  cbvopab2v  4107  unopab  4109  iunopab  4313  abnex  4479  uniuni  4483  ruv  4583  rabxp  4697  dfdm3  4850  dfrn2  4851  dfrn3  4852  dfdm4  4855  dfdmf  4856  dmun  4870  dmopab  4874  dmopabss  4875  dmopab3  4876  dfrnf  4904  rnopab  4910  rnmpt  4911  dfima2  5008  dfima3  5009  imadmrn  5016  imai  5022  args  5035  mptpreima  5160  dfiota2  5217  cbviota  5221  sb8iota  5223  dffv4g  5552  dfimafn2  5607  fnasrn  5737  fnasrng  5739  elabrex  5801  elabrexg  5802  abrexco  5803  dfoprab2  5966  cbvoprab2  5992  dmoprab  6000  rnoprab  6002  rnoprab2  6003  fnrnov  6066  abrexex2g  6174  abrexex2  6178  abexssex  6179  abexex  6180  oprabrexex2  6184  dfopab2  6244  cnvoprab  6289  tfr1onlemaccex  6403  tfrcllemaccex  6416  tfrcldm  6418  frec0g  6452  frecsuc  6462  snec  6652  pmex  6709  dfixp  6756  cbvixp  6771  caucvgprprlemmu  7757  caucvgsr  7864  pitonnlem1  7907  mertenslem2  11682  4sqlemafi  12536  dfrhm2  13653  toponsspwpwg  14201  tgval2  14230  2lgslem1b  15246  if0ab  15367  bdcuni  15438  bj-dfom  15495