Theorem abbidv 2348

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  {cab 2216

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223

This theorem is referenced by:  rabbidva2  2785  cdeqab  3020  sbceqbid  3037  csbeq1  3129  sbcel12g  3141  sbceqg  3142  csbeq2  3150  csbeq2d  3151  csbnestgf  3179  csbprc  3539  ifbi  3625  pweq  3654  sneq  3679  csbsng  3729  rabsn  3735  dfopg  3859  opeq1  3861  opeq2  3862  csbunig  3900  unieq  3901  inteq  3930  iineq1  3983  iineq2  3986  dfiin2g  4002  iinrabm  4032  iinxprg  4044  opabbid  4153  dcextest  4678  csbxpg  4806  csbdmg  4924  imasng  5100  csbrng  5197  iotaeq  5294  iotabi  5295  dfimafn  5694  fnsnfv  5705  fndmin  5754  fliftf  5942  oprabbid  6076  recseq  6474  freceq1  6560  freceq2  6561  frec0g  6565  freccllem  6570  frecfcllem  6572  frecsuclem  6574  frecsuc  6575  qseq1  6754  qseq2  6755  qsinxp  6782  mapvalg  6829  ixpsnval  6872  ixpeq1  6880  snexxph  7151  fival  7171  acneq  7419  prplnqu  7842  cauappcvgprlemlim  7883  caucvgprprlemell  7907  caucvgprprlemelu  7908  caucvgprprlemcbv  7909  caucvgprprlemval  7910  caucvgprprlemnkeqj  7912  caucvgprprlemml  7916  caucvgprprlemmu  7917  caucvgprprlemopl  7919  caucvgprprlemlol  7920  caucvgprprlemopu  7921  caucvgprprlemloc  7925  caucvgprprlemclphr  7927  caucvgprprlemexbt  7928  caucvgprprlem1  7931  caucvgprprlem2  7932  caucvgsr  8024  pitonnlem2  8069  pitonn  8070  recidpipr  8078  nntopi  8116  axcaucvglemval  8119  csbwrdg  11149  shftlem  11396  shftfibg  11400  shftdm  11402  shftfib  11403  negfi  11808  tgval  13365  ptex  13367  eqglact  13832  isghm  13850  ixpsnbasval  14501  plyval  15482  vtxdfifiun  16174