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 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402  {cab 2224

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 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 theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231

This theorem is referenced 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  3719  csbsng  3769  rabsn  3775  dfopg  3900  opeq1  3902  opeq2  3903  csbunig  3941  unieq  3942  inteq  3971  iineq1  4024  iineq2  4027  dfiin2g  4043  iinrabm  4073  iinxprg  4085  opabbid  4194  dcextest  4726  csbxpg  4854  csbdmg  4973  imasng  5150  csbrng  5247  iotaeq  5344  iotabi  5345  dfimafn  5748  fnsnfv  5759  fndmin  5810  dfimafnf  5949  fliftf  5999  oprabbid  6135  recseq  6571  freceq1  6657  freceq2  6658  frec0g  6662  freccllem  6667  frecfcllem  6669  frecsuclem  6671  frecsuc  6672  qseq1  6851  qseq2  6852  qsinxp  6879  mapvalg  6926  ixpsnval  6977  ixpeq1  6985  snexxph  7261  fival  7298  acneq  7552  prplnqu  7981  cauappcvgprlemlim  8022  caucvgprprlemell  8046  caucvgprprlemelu  8047  caucvgprprlemcbv  8048  caucvgprprlemval  8049  caucvgprprlemnkeqj  8051  caucvgprprlemml  8055  caucvgprprlemmu  8056  caucvgprprlemopl  8058  caucvgprprlemlol  8059  caucvgprprlemopu  8060  caucvgprprlemloc  8064  caucvgprprlemclphr  8066  caucvgprprlemexbt  8067  caucvgprprlem1  8070  caucvgprprlem2  8071  caucvgsr  8163  pitonnlem2  8208  pitonn  8209  recidpipr  8217  nntopi  8255  axcaucvglemval  8258  hashf1lem2  11269  hashf1  11270  hashfac  11271  csbwrdg  11317  shftlem  11564  shftfibg  11568  shftdm  11570  shftfib  11571  negfi  11977  tgval  13599  ptex  13601  eqglact  14011  isghm  14029  ixpsnbasval  14786  plyval  15816  vtxdfifiun  16521