Theorem abbidv 2358

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402  {cab 2224

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231

This theorem is used by:  rabbidva2  2805  cdeqab  3041  sbceqbid  3058  csbeq1  3150  sbcel12g  3162  sbceqg  3163  csbeq2  3171  csbeq2d  3172  csbnestgf  3200  csbprc  3572  ifbi  3661  pweq  3691  sneq  3720  csbsng  3770  rabsn  3776  dfopg  3902  opeq1  3904  opeq2  3905  csbunig  3943  unieq  3944  inteq  3973  iineq1  4026  iineq2  4029  dfiin2g  4045  iinrabm  4075  iinxprg  4087  opabbid  4197  dcextest  4730  csbxpg  4858  csbdmg  4977  imasng  5155  csbrng  5252  iotaeq  5349  iotabi  5350  dfimafn  5754  fnsnfv  5765  fndmin  5819  dfimafnf  5958  fliftf  6008  oprabbid  6144  recseq  6581  freceq1  6667  freceq2  6668  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  qseq1  6861  qseq2  6862  qsinxp  6889  mapvalg  6936  ixpsnval  6988  ixpeq1  6996  snexxph  7273  fival  7310  acneq  7565  prplnqu  7994  cauappcvgprlemlim  8035  caucvgprprlemell  8059  caucvgprprlemelu  8060  caucvgprprlemcbv  8061  caucvgprprlemval  8062  caucvgprprlemnkeqj  8064  caucvgprprlemml  8068  caucvgprprlemmu  8069  caucvgprprlemopl  8071  caucvgprprlemlol  8072  caucvgprprlemopu  8073  caucvgprprlemloc  8077  caucvgprprlemclphr  8079  caucvgprprlemexbt  8080  caucvgprprlem1  8083  caucvgprprlem2  8084  caucvgsr  8176  pitonnlem2  8221  pitonn  8222  recidpipr  8230  nntopi  8268  axcaucvglemval  8271  hashf1lem2  11309  hashf1  11310  hashfac  11311  csbwrdg  11357  shftlem  11604  shftfibg  11608  shftdm  11610  shftfib  11611  negfi  12018  tgval  13676  ptex  13678  eqglact  14088  isghm  14106  ixpsnbasval  14913  plyval  15970  vtxdfifiun  16755