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  4196  dcextest  4728  csbxpg  4856  csbdmg  4975  imasng  5152  csbrng  5249  iotaeq  5346  iotabi  5347  dfimafn  5751  fnsnfv  5762  fndmin  5816  dfimafnf  5955  fliftf  6005  oprabbid  6141  recseq  6577  freceq1  6663  freceq2  6664  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  qseq1  6857  qseq2  6858  qsinxp  6885  mapvalg  6932  ixpsnval  6983  ixpeq1  6991  snexxph  7267  fival  7304  acneq  7559  prplnqu  7988  cauappcvgprlemlim  8029  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkeqj  8058  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlem1  8077  caucvgprprlem2  8078  caucvgsr  8170  pitonnlem2  8215  pitonn  8216  recidpipr  8224  nntopi  8262  axcaucvglemval  8265  hashf1lem2  11301  hashf1  11302  hashfac  11303  csbwrdg  11349  shftlem  11596  shftfibg  11600  shftdm  11602  shftfib  11603  negfi  12010  tgval  13667  ptex  13669  eqglact  14079  isghm  14097  ixpsnbasval  14854  plyval  15885  vtxdfifiun  16660