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 1500	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 105   = wceq 1397  {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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

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

This theorem is referenced by:  rabswap  2712  rabbiia  2788  rabab  2824  csb2  3129  cbvcsbw  3131  cbvcsb  3132  csbid  3135  csbco  3137  csbcow  3138  cbvreucsf  3192  unrab  3478  inrab  3479  inrab2  3480  difrab  3481  rabun2  3486  dfnul3  3497  rab0  3523  rabsnifsb  3737  tprot  3764  pw0  3820  dfuni2  3895  unipr  3907  dfint2  3930  int0  3942  dfiunv2  4006  cbviun  4007  cbviin  4008  iunrab  4018  iunid  4026  viin  4030  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  cbvopab2v  4166  unopab  4168  iunopab  4376  abnex  4544  uniuni  4548  ruv  4648  rabxp  4763  dfdm3  4917  dfrn2  4918  dfrn3  4919  dfdm4  4923  dfdmf  4924  dmun  4938  dmopab  4942  dmopabss  4943  dmopab3  4944  dfrnf  4973  rnopab  4979  rnmpt  4980  dfima2  5078  dfima3  5079  imadmrn  5086  imai  5092  args  5105  mptpreima  5230  dfiota2  5287  cbviota  5291  cbviotavw  5292  sb8iota  5294  dffv4g  5636  dfimafn2  5695  fnasrn  5825  fnasrng  5827  elabrex  5897  elabrexg  5898  abrexco  5899  dfoprab2  6067  cbvoprab2  6093  dmoprab  6101  rnoprab  6103  rnoprab2  6104  fnrnov  6167  abrexex2g  6281  abrexex2  6285  abexssex  6286  abexex  6287  oprabrexex2  6291  dfopab2  6351  cnvoprab  6398  tfr1onlemaccex  6513  tfrcllemaccex  6526  tfrcldm  6528  frec0g  6562  frecsuc  6572  snec  6764  pmex  6821  dfixp  6868  cbvixp  6883  caucvgprprlemmu  7914  caucvgsr  8021  pitonnlem1  8064  mertenslem2  12096  4sqlemafi  12967  dfrhm2  14167  toponsspwpwg  14745  tgval2  14774  2lgslem1b  15817  if0ab  16401  bdcuni  16471  bj-dfom  16528