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  5826  fnasrng  5828  elabrex  5898  elabrexg  5899  abrexco  5900  dfoprab2  6068  cbvoprab2  6094  dmoprab  6102  rnoprab  6104  rnoprab2  6105  fnrnov  6168  abrexex2g  6282  abrexex2  6286  abexssex  6287  abexex  6288  oprabrexex2  6292  dfopab2  6352  cnvoprab  6399  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfrcldm  6529  frec0g  6563  frecsuc  6573  snec  6765  pmex  6822  dfixp  6869  cbvixp  6884  caucvgprprlemmu  7915  caucvgsr  8022  pitonnlem1  8065  mertenslem2  12102  4sqlemafi  12973  dfrhm2  14174  toponsspwpwg  14752  tgval2  14781  2lgslem1b  15824  if0ab  16427  bdcuni  16497  bj-dfom  16554