Theorem abbii 2320

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

Syntax hints:   ↔ wb 105   = wceq 1372  {cab 2190

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197

This theorem is referenced by:  rabswap  2684  rabbiia  2756  rabab  2792  csb2  3094  cbvcsbw  3096  cbvcsb  3097  csbid  3100  csbco  3102  csbcow  3103  cbvreucsf  3157  unrab  3443  inrab  3444  inrab2  3445  difrab  3446  rabun2  3451  dfnul3  3462  rab0  3488  tprot  3725  pw0  3779  dfuni2  3851  unipr  3863  dfint2  3886  int0  3898  dfiunv2  3962  cbviun  3963  cbviin  3964  iunrab  3974  iunid  3982  viin  3986  cbvopab  4114  cbvopab1  4116  cbvopab2  4117  cbvopab1s  4118  cbvopab2v  4120  unopab  4122  iunopab  4327  abnex  4493  uniuni  4497  ruv  4597  rabxp  4711  dfdm3  4864  dfrn2  4865  dfrn3  4866  dfdm4  4869  dfdmf  4870  dmun  4884  dmopab  4888  dmopabss  4889  dmopab3  4890  dfrnf  4918  rnopab  4924  rnmpt  4925  dfima2  5023  dfima3  5024  imadmrn  5031  imai  5037  args  5050  mptpreima  5175  dfiota2  5232  cbviota  5236  sb8iota  5238  dffv4g  5572  dfimafn2  5627  fnasrn  5757  fnasrng  5759  elabrex  5825  elabrexg  5826  abrexco  5827  dfoprab2  5991  cbvoprab2  6017  dmoprab  6025  rnoprab  6027  rnoprab2  6028  fnrnov  6091  abrexex2g  6204  abrexex2  6208  abexssex  6209  abexex  6210  oprabrexex2  6214  dfopab2  6274  cnvoprab  6319  tfr1onlemaccex  6433  tfrcllemaccex  6446  tfrcldm  6448  frec0g  6482  frecsuc  6492  snec  6682  pmex  6739  dfixp  6786  cbvixp  6801  caucvgprprlemmu  7807  caucvgsr  7914  pitonnlem1  7957  mertenslem2  11789  4sqlemafi  12660  dfrhm2  13858  toponsspwpwg  14436  tgval2  14465  2lgslem1b  15508  if0ab  15674  bdcuni  15745  bj-dfom  15802