Theorem abbidv 2347

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  {cab 2215

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222

This theorem is referenced by:  rabbidva2  2786  cdeqab  3018  sbceqbid  3035  csbeq1  3127  sbcel12g  3139  sbceqg  3140  csbeq2  3148  csbeq2d  3149  csbnestgf  3177  csbprc  3537  ifbi  3623  pweq  3652  sneq  3677  csbsng  3727  rabsn  3733  dfopg  3855  opeq1  3857  opeq2  3858  csbunig  3896  unieq  3897  inteq  3926  iineq1  3979  iineq2  3982  dfiin2g  3998  iinrabm  4028  iinxprg  4040  opabbid  4149  dcextest  4673  csbxpg  4800  csbdmg  4917  imasng  5093  csbrng  5190  iotaeq  5287  iotabi  5288  dfimafn  5684  fnsnfv  5695  fndmin  5744  fliftf  5929  oprabbid  6063  recseq  6458  freceq1  6544  freceq2  6545  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  qseq1  6738  qseq2  6739  qsinxp  6766  mapvalg  6813  ixpsnval  6856  ixpeq1  6864  snexxph  7125  fival  7145  acneq  7392  prplnqu  7815  cauappcvgprlemlim  7856  caucvgprprlemell  7880  caucvgprprlemelu  7881  caucvgprprlemcbv  7882  caucvgprprlemval  7883  caucvgprprlemnkeqj  7885  caucvgprprlemml  7889  caucvgprprlemmu  7890  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemopu  7894  caucvgprprlemloc  7898  caucvgprprlemclphr  7900  caucvgprprlemexbt  7901  caucvgprprlem1  7904  caucvgprprlem2  7905  caucvgsr  7997  pitonnlem2  8042  pitonn  8043  recidpipr  8051  nntopi  8089  axcaucvglemval  8092  csbwrdg  11109  shftlem  11335  shftfibg  11339  shftdm  11341  shftfib  11342  negfi  11747  tgval  13303  ptex  13305  eqglact  13770  isghm  13788  ixpsnbasval  14438  plyval  15414