Theorem abbidv 2295

Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.)

Hypothesis

Ref	Expression
abbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
abbidv	⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem abbidv

Step	Hyp	Ref	Expression
1		nfv 1528	. 2 ⊢ Ⅎ𝑥𝜑
2		abbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	abbid 2294	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353  {cab 2163

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170

This theorem is referenced by:  rabbidva2  2726  cdeqab  2954  sbceqbid  2971  csbeq1  3062  sbcel12g  3074  sbceqg  3075  csbeq2  3083  csbeq2d  3084  csbnestgf  3111  csbprc  3470  ifbi  3556  pweq  3580  sneq  3605  csbsng  3655  rabsn  3661  dfopg  3778  opeq1  3780  opeq2  3781  csbunig  3819  unieq  3820  inteq  3849  iineq1  3902  iineq2  3905  dfiin2g  3921  iinrabm  3951  iinxprg  3963  opabbid  4070  dcextest  4582  csbxpg  4709  csbdmg  4823  imasng  4995  csbrng  5092  iotaeq  5188  iotabi  5189  dfimafn  5566  fnsnfv  5577  fndmin  5625  fliftf  5802  oprabbid  5930  recseq  6309  freceq1  6395  freceq2  6396  frec0g  6400  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecsuc  6410  qseq1  6585  qseq2  6586  qsinxp  6613  mapvalg  6660  ixpsnval  6703  ixpeq1  6711  snexxph  6951  fival  6971  prplnqu  7621  cauappcvgprlemlim  7662  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemnkeqj  7691  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemloc  7704  caucvgprprlemclphr  7706  caucvgprprlemexbt  7707  caucvgprprlem1  7710  caucvgprprlem2  7711  caucvgsr  7803  pitonnlem2  7848  pitonn  7849  recidpipr  7857  nntopi  7895  axcaucvglemval  7898  shftlem  10827  shftfibg  10831  shftdm  10833  shftfib  10834  negfi  11238  tgval  12716  ptex  12718  eqglact  13089