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  tprot  3760  pw0  3816  dfuni2  3891  unipr  3903  dfint2  3926  int0  3938  dfiunv2  4002  cbviun  4003  cbviin  4004  iunrab  4014  iunid  4022  viin  4026  cbvopab  4156  cbvopab1  4158  cbvopab2  4159  cbvopab1s  4160  cbvopab2v  4162  unopab  4164  iunopab  4372  abnex  4540  uniuni  4544  ruv  4644  rabxp  4759  dfdm3  4913  dfrn2  4914  dfrn3  4915  dfdm4  4919  dfdmf  4920  dmun  4934  dmopab  4938  dmopabss  4939  dmopab3  4940  dfrnf  4969  rnopab  4975  rnmpt  4976  dfima2  5074  dfima3  5075  imadmrn  5082  imai  5088  args  5101  mptpreima  5226  dfiota2  5283  cbviota  5287  cbviotavw  5288  sb8iota  5290  dffv4g  5630  dfimafn2  5689  fnasrn  5819  fnasrng  5821  elabrex  5891  elabrexg  5892  abrexco  5893  dfoprab2  6061  cbvoprab2  6087  dmoprab  6095  rnoprab  6097  rnoprab2  6098  fnrnov  6161  abrexex2g  6275  abrexex2  6279  abexssex  6280  abexex  6281  oprabrexex2  6285  dfopab2  6345  cnvoprab  6392  tfr1onlemaccex  6507  tfrcllemaccex  6520  tfrcldm  6522  frec0g  6556  frecsuc  6566  snec  6758  pmex  6815  dfixp  6862  cbvixp  6877  caucvgprprlemmu  7903  caucvgsr  8010  pitonnlem1  8053  mertenslem2  12084  4sqlemafi  12955  dfrhm2  14155  toponsspwpwg  14733  tgval2  14762  2lgslem1b  15805  if0ab  16311  bdcuni  16381  bj-dfom  16438