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  2786  rabab  2822  csb2  3127  cbvcsbw  3129  cbvcsb  3130  csbid  3133  csbco  3135  csbcow  3136  cbvreucsf  3190  unrab  3476  inrab  3477  inrab2  3478  difrab  3479  rabun2  3484  dfnul3  3495  rab0  3521  rabsnifsb  3735  tprot  3762  pw0  3818  dfuni2  3893  unipr  3905  dfint2  3928  int0  3940  dfiunv2  4004  cbviun  4005  cbviin  4006  iunrab  4016  iunid  4024  viin  4028  cbvopab  4158  cbvopab1  4160  cbvopab2  4161  cbvopab1s  4162  cbvopab2v  4164  unopab  4166  iunopab  4374  abnex  4542  uniuni  4546  ruv  4646  rabxp  4761  dfdm3  4915  dfrn2  4916  dfrn3  4917  dfdm4  4921  dfdmf  4922  dmun  4936  dmopab  4940  dmopabss  4941  dmopab3  4942  dfrnf  4971  rnopab  4977  rnmpt  4978  dfima2  5076  dfima3  5077  imadmrn  5084  imai  5090  args  5103  mptpreima  5228  dfiota2  5285  cbviota  5289  cbviotavw  5290  sb8iota  5292  dffv4g  5632  dfimafn2  5691  fnasrn  5821  fnasrng  5823  elabrex  5893  elabrexg  5894  abrexco  5895  dfoprab2  6063  cbvoprab2  6089  dmoprab  6097  rnoprab  6099  rnoprab2  6100  fnrnov  6163  abrexex2g  6277  abrexex2  6281  abexssex  6282  abexex  6283  oprabrexex2  6287  dfopab2  6347  cnvoprab  6394  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfrcldm  6524  frec0g  6558  frecsuc  6568  snec  6760  pmex  6817  dfixp  6864  cbvixp  6879  caucvgprprlemmu  7905  caucvgsr  8012  pitonnlem1  8055  mertenslem2  12087  4sqlemafi  12958  dfrhm2  14158  toponsspwpwg  14736  tgval2  14765  2lgslem1b  15808  if0ab  16337  bdcuni  16407  bj-dfom  16464