Theorem abbii 2322

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

Syntax hints:   ↔ wb 105   = wceq 1373  {cab 2192

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199

This theorem is referenced by:  rabswap  2686  rabbiia  2758  rabab  2795  csb2  3099  cbvcsbw  3101  cbvcsb  3102  csbid  3105  csbco  3107  csbcow  3108  cbvreucsf  3162  unrab  3448  inrab  3449  inrab2  3450  difrab  3451  rabun2  3456  dfnul3  3467  rab0  3493  tprot  3731  pw0  3786  dfuni2  3858  unipr  3870  dfint2  3893  int0  3905  dfiunv2  3969  cbviun  3970  cbviin  3971  iunrab  3981  iunid  3989  viin  3993  cbvopab  4123  cbvopab1  4125  cbvopab2  4126  cbvopab1s  4127  cbvopab2v  4129  unopab  4131  iunopab  4336  abnex  4502  uniuni  4506  ruv  4606  rabxp  4720  dfdm3  4873  dfrn2  4874  dfrn3  4875  dfdm4  4879  dfdmf  4880  dmun  4894  dmopab  4898  dmopabss  4899  dmopab3  4900  dfrnf  4928  rnopab  4934  rnmpt  4935  dfima2  5033  dfima3  5034  imadmrn  5041  imai  5047  args  5060  mptpreima  5185  dfiota2  5242  cbviota  5246  sb8iota  5248  dffv4g  5586  dfimafn2  5641  fnasrn  5771  fnasrng  5773  elabrex  5839  elabrexg  5840  abrexco  5841  dfoprab2  6005  cbvoprab2  6031  dmoprab  6039  rnoprab  6041  rnoprab2  6042  fnrnov  6105  abrexex2g  6218  abrexex2  6222  abexssex  6223  abexex  6224  oprabrexex2  6228  dfopab2  6288  cnvoprab  6333  tfr1onlemaccex  6447  tfrcllemaccex  6460  tfrcldm  6462  frec0g  6496  frecsuc  6506  snec  6696  pmex  6753  dfixp  6800  cbvixp  6815  caucvgprprlemmu  7828  caucvgsr  7935  pitonnlem1  7978  mertenslem2  11922  4sqlemafi  12793  dfrhm2  13991  toponsspwpwg  14569  tgval2  14598  2lgslem1b  15641  if0ab  15880  bdcuni  15950  bj-dfom  16007