Theorem abbidv 2350

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 1577	. 2 ⊢ Ⅎ𝑥𝜑
2		abbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	abbid 2348	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  {cab 2217

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224

This theorem is referenced by:  rabbidva2  2787  cdeqab  3022  sbceqbid  3039  csbeq1  3131  sbcel12g  3143  sbceqg  3144  csbeq2  3152  csbeq2d  3153  csbnestgf  3181  csbprc  3542  ifbi  3630  pweq  3659  sneq  3684  csbsng  3734  rabsn  3740  dfopg  3865  opeq1  3867  opeq2  3868  csbunig  3906  unieq  3907  inteq  3936  iineq1  3989  iineq2  3992  dfiin2g  4008  iinrabm  4038  iinxprg  4050  opabbid  4159  dcextest  4685  csbxpg  4813  csbdmg  4931  imasng  5108  csbrng  5205  iotaeq  5302  iotabi  5303  dfimafn  5703  fnsnfv  5714  fndmin  5763  fliftf  5950  oprabbid  6084  recseq  6515  freceq1  6601  freceq2  6602  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  qseq1  6795  qseq2  6796  qsinxp  6823  mapvalg  6870  ixpsnval  6913  ixpeq1  6921  snexxph  7192  fival  7212  acneq  7460  prplnqu  7883  cauappcvgprlemlim  7924  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemnkeqj  7953  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  caucvgprprlem1  7972  caucvgprprlem2  7973  caucvgsr  8065  pitonnlem2  8110  pitonn  8111  recidpipr  8119  nntopi  8157  axcaucvglemval  8160  csbwrdg  11190  shftlem  11437  shftfibg  11441  shftdm  11443  shftfib  11444  negfi  11849  tgval  13406  ptex  13408  eqglact  13873  isghm  13891  ixpsnbasval  14542  plyval  15523  vtxdfifiun  16218