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  5567  fnsnfv  5578  fndmin  5626  fliftf  5803  oprabbid  5931  recseq  6310  freceq1  6396  freceq2  6397  frec0g  6401  freccllem  6406  frecfcllem  6408  frecsuclem  6410  frecsuc  6411  qseq1  6586  qseq2  6587  qsinxp  6614  mapvalg  6661  ixpsnval  6704  ixpeq1  6712  snexxph  6952  fival  6972  prplnqu  7622  cauappcvgprlemlim  7663  caucvgprprlemell  7687  caucvgprprlemelu  7688  caucvgprprlemcbv  7689  caucvgprprlemval  7690  caucvgprprlemnkeqj  7692  caucvgprprlemml  7696  caucvgprprlemmu  7697  caucvgprprlemopl  7699  caucvgprprlemlol  7700  caucvgprprlemopu  7701  caucvgprprlemloc  7705  caucvgprprlemclphr  7707  caucvgprprlemexbt  7708  caucvgprprlem1  7711  caucvgprprlem2  7712  caucvgsr  7804  pitonnlem2  7849  pitonn  7850  recidpipr  7858  nntopi  7896  axcaucvglemval  7899  shftlem  10828  shftfibg  10832  shftdm  10834  shftfib  10835  negfi  11239  tgval  12717  ptex  12719  eqglact  13099  ixpsnbasval  13590