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  4674  csbxpg  4802  csbdmg  4920  imasng  5096  csbrng  5193  iotaeq  5290  iotabi  5291  dfimafn  5687  fnsnfv  5698  fndmin  5747  fliftf  5932  oprabbid  6066  recseq  6463  freceq1  6549  freceq2  6550  frec0g  6554  freccllem  6559  frecfcllem  6561  frecsuclem  6563  frecsuc  6564  qseq1  6743  qseq2  6744  qsinxp  6771  mapvalg  6818  ixpsnval  6861  ixpeq1  6869  snexxph  7133  fival  7153  acneq  7400  prplnqu  7823  cauappcvgprlemlim  7864  caucvgprprlemell  7888  caucvgprprlemelu  7889  caucvgprprlemcbv  7890  caucvgprprlemval  7891  caucvgprprlemnkeqj  7893  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemopu  7902  caucvgprprlemloc  7906  caucvgprprlemclphr  7908  caucvgprprlemexbt  7909  caucvgprprlem1  7912  caucvgprprlem2  7913  caucvgsr  8005  pitonnlem2  8050  pitonn  8051  recidpipr  8059  nntopi  8097  axcaucvglemval  8100  csbwrdg  11119  shftlem  11348  shftfibg  11352  shftdm  11354  shftfib  11355  negfi  11760  tgval  13316  ptex  13318  eqglact  13783  isghm  13801  ixpsnbasval  14451  plyval  15427  vtxdfifiun  16083