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  3082  cbvcsbw  3084  cbvcsb  3085  csbid  3088  csbco  3090  csbcow  3091  cbvreucsf  3145  unrab  3430  inrab  3431  inrab2  3432  difrab  3433  rabun2  3438  dfnul3  3449  rab0  3475  tprot  3711  pw0  3765  dfuni2  3837  unipr  3849  dfint2  3872  int0  3884  dfiunv2  3948  cbviun  3949  cbviin  3950  iunrab  3960  iunid  3968  viin  3972  cbvopab  4100  cbvopab1  4102  cbvopab2  4103  cbvopab1s  4104  cbvopab2v  4106  unopab  4108  iunopab  4312  abnex  4478  uniuni  4482  ruv  4582  rabxp  4696  dfdm3  4849  dfrn2  4850  dfrn3  4851  dfdm4  4854  dfdmf  4855  dmun  4869  dmopab  4873  dmopabss  4874  dmopab3  4875  dfrnf  4903  rnopab  4909  rnmpt  4910  dfima2  5007  dfima3  5008  imadmrn  5015  imai  5021  args  5034  mptpreima  5159  dfiota2  5216  cbviota  5220  sb8iota  5222  dffv4g  5551  dfimafn2  5606  fnasrn  5736  fnasrng  5738  elabrex  5800  elabrexg  5801  abrexco  5802  dfoprab2  5965  cbvoprab2  5991  dmoprab  5999  rnoprab  6001  rnoprab2  6002  fnrnov  6064  abrexex2g  6172  abrexex2  6176  abexssex  6177  abexex  6178  oprabrexex2  6182  dfopab2  6242  cnvoprab  6287  tfr1onlemaccex  6401  tfrcllemaccex  6414  tfrcldm  6416  frec0g  6450  frecsuc  6460  snec  6650  pmex  6707  dfixp  6754  cbvixp  6769  caucvgprprlemmu  7755  caucvgsr  7862  pitonnlem1  7905  mertenslem2  11679  4sqlemafi  12533  dfrhm2  13650  toponsspwpwg  14190  tgval2  14219  if0ab  15297  bdcuni  15368  bj-dfom  15425