Theorem abbii 2347

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

Syntax hints:   ↔ wb 105   = wceq 1398  {cab 2217

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224

This theorem is referenced by:  rabswap  2713  rabbiia  2789  rabab  2825  csb2  3130  cbvcsbw  3132  cbvcsb  3133  csbid  3136  csbco  3138  csbcow  3139  cbvreucsf  3193  unrab  3480  inrab  3481  inrab2  3482  difrab  3483  rabun2  3488  dfnul3  3499  rab0  3525  rabsnifsb  3741  tprot  3768  pw0  3825  dfuni2  3900  unipr  3912  dfint2  3935  int0  3947  dfiunv2  4011  cbviun  4012  cbviin  4013  iunrab  4023  iunid  4031  viin  4035  cbvopab  4165  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab2v  4171  unopab  4173  iunopab  4382  abnex  4550  uniuni  4554  ruv  4654  rabxp  4769  dfdm3  4923  dfrn2  4924  dfrn3  4925  dfdm4  4929  dfdmf  4930  dmun  4944  dmopab  4948  dmopabss  4949  dmopab3  4950  dfrnf  4979  rnopab  4985  rnmpt  4986  dfima2  5084  dfima3  5085  imadmrn  5092  imai  5099  args  5112  mptpreima  5237  dfiota2  5294  cbviota  5298  cbviotavw  5299  sb8iota  5301  dffv4g  5645  dfimafn2  5704  fnasrn  5834  fnasrng  5836  elabrex  5908  elabrexg  5909  abrexco  5910  dfoprab2  6078  cbvoprab2  6104  dmoprab  6112  rnoprab  6114  rnoprab2  6115  fnrnov  6178  abrexex2g  6291  abrexex2  6295  abexssex  6296  abexex  6297  oprabrexex2  6301  dfopab2  6361  cnvoprab  6408  cnvimadfsn  6423  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcldm  6572  frec0g  6606  frecsuc  6616  snec  6808  pmex  6865  dfixp  6912  cbvixp  6927  caucvgprprlemmu  7958  caucvgsr  8065  pitonnlem1  8108  mertenslem2  12160  4sqlemafi  13031  dfrhm2  14232  toponsspwpwg  14816  tgval2  14845  2lgslem1b  15891  bdcuni  16575  bj-dfom  16632