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  2724  cdeqab  2952  sbceqbid  2969  csbeq1  3060  sbcel12g  3072  sbceqg  3073  csbeq2  3081  csbeq2d  3082  csbnestgf  3109  csbprc  3468  ifbi  3554  pweq  3578  sneq  3603  csbsng  3653  rabsn  3659  dfopg  3776  opeq1  3778  opeq2  3779  csbunig  3817  unieq  3818  inteq  3847  iineq1  3900  iineq2  3903  dfiin2g  3919  iinrabm  3949  iinxprg  3961  opabbid  4068  dcextest  4580  csbxpg  4707  csbdmg  4821  imasng  4993  csbrng  5090  iotaeq  5186  iotabi  5187  dfimafn  5564  fnsnfv  5575  fndmin  5623  fliftf  5799  oprabbid  5927  recseq  6306  freceq1  6392  freceq2  6393  frec0g  6397  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecsuc  6407  qseq1  6582  qseq2  6583  qsinxp  6610  mapvalg  6657  ixpsnval  6700  ixpeq1  6708  snexxph  6948  fival  6968  prplnqu  7618  cauappcvgprlemlim  7659  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  caucvgsr  7800  pitonnlem2  7845  pitonn  7846  recidpipr  7854  nntopi  7892  axcaucvglemval  7895  shftlem  10824  shftfibg  10828  shftdm  10830  shftfib  10831  negfi  11235  tgval  12710  ptex  12712  eqglact  13082