Theorem abbii 2345

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

Syntax hints:   ↔ wb 105   = wceq 1395  {cab 2215

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222

This theorem is referenced by:  rabswap  2710  rabbiia  2784  rabab  2821  csb2  3126  cbvcsbw  3128  cbvcsb  3129  csbid  3132  csbco  3134  csbcow  3135  cbvreucsf  3189  unrab  3475  inrab  3476  inrab2  3477  difrab  3478  rabun2  3483  dfnul3  3494  rab0  3520  tprot  3759  pw0  3815  dfuni2  3890  unipr  3902  dfint2  3925  int0  3937  dfiunv2  4001  cbviun  4002  cbviin  4003  iunrab  4013  iunid  4021  viin  4025  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab2v  4161  unopab  4163  iunopab  4370  abnex  4538  uniuni  4542  ruv  4642  rabxp  4756  dfdm3  4909  dfrn2  4910  dfrn3  4911  dfdm4  4915  dfdmf  4916  dmun  4930  dmopab  4934  dmopabss  4935  dmopab3  4936  dfrnf  4965  rnopab  4971  rnmpt  4972  dfima2  5070  dfima3  5071  imadmrn  5078  imai  5084  args  5097  mptpreima  5222  dfiota2  5279  cbviota  5283  cbviotavw  5284  sb8iota  5286  dffv4g  5626  dfimafn2  5685  fnasrn  5815  fnasrng  5817  elabrex  5887  elabrexg  5888  abrexco  5889  dfoprab2  6057  cbvoprab2  6083  dmoprab  6091  rnoprab  6093  rnoprab2  6094  fnrnov  6157  abrexex2g  6271  abrexex2  6275  abexssex  6276  abexex  6277  oprabrexex2  6281  dfopab2  6341  cnvoprab  6386  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcldm  6515  frec0g  6549  frecsuc  6559  snec  6751  pmex  6808  dfixp  6855  cbvixp  6870  caucvgprprlemmu  7893  caucvgsr  8000  pitonnlem1  8043  mertenslem2  12062  4sqlemafi  12933  dfrhm2  14133  toponsspwpwg  14711  tgval2  14740  2lgslem1b  15783  if0ab  16224  bdcuni  16294  bj-dfom  16351