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  3814  dfuni2  3889  unipr  3901  dfint2  3924  int0  3936  dfiunv2  4000  cbviun  4001  cbviin  4002  iunrab  4012  iunid  4020  viin  4024  cbvopab  4154  cbvopab1  4156  cbvopab2  4157  cbvopab1s  4158  cbvopab2v  4160  unopab  4162  iunopab  4369  abnex  4537  uniuni  4541  ruv  4641  rabxp  4755  dfdm3  4908  dfrn2  4909  dfrn3  4910  dfdm4  4914  dfdmf  4915  dmun  4929  dmopab  4933  dmopabss  4934  dmopab3  4935  dfrnf  4964  rnopab  4970  rnmpt  4971  dfima2  5069  dfima3  5070  imadmrn  5077  imai  5083  args  5096  mptpreima  5221  dfiota2  5278  cbviota  5282  cbviotavw  5283  sb8iota  5285  dffv4g  5623  dfimafn2  5682  fnasrn  5812  fnasrng  5814  elabrex  5880  elabrexg  5881  abrexco  5882  dfoprab2  6050  cbvoprab2  6076  dmoprab  6084  rnoprab  6086  rnoprab2  6087  fnrnov  6150  abrexex2g  6263  abrexex2  6267  abexssex  6268  abexex  6269  oprabrexex2  6273  dfopab2  6333  cnvoprab  6378  tfr1onlemaccex  6492  tfrcllemaccex  6505  tfrcldm  6507  frec0g  6541  frecsuc  6551  snec  6741  pmex  6798  dfixp  6845  cbvixp  6860  caucvgprprlemmu  7878  caucvgsr  7985  pitonnlem1  8028  mertenslem2  12042  4sqlemafi  12913  dfrhm2  14112  toponsspwpwg  14690  tgval2  14719  2lgslem1b  15762  if0ab  16127  bdcuni  16197  bj-dfom  16254