Theorem abbidv 2349

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224

This theorem is referenced by:  rabbidva2  2786  cdeqab  3021  sbceqbid  3038  csbeq1  3130  sbcel12g  3142  sbceqg  3143  csbeq2  3151  csbeq2d  3152  csbnestgf  3180  csbprc  3540  ifbi  3626  pweq  3655  sneq  3680  csbsng  3730  rabsn  3736  dfopg  3860  opeq1  3862  opeq2  3863  csbunig  3901  unieq  3902  inteq  3931  iineq1  3984  iineq2  3987  dfiin2g  4003  iinrabm  4033  iinxprg  4045  opabbid  4154  dcextest  4679  csbxpg  4807  csbdmg  4925  imasng  5101  csbrng  5198  iotaeq  5295  iotabi  5296  dfimafn  5694  fnsnfv  5705  fndmin  5754  fliftf  5940  oprabbid  6074  recseq  6472  freceq1  6558  freceq2  6559  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  qseq1  6752  qseq2  6753  qsinxp  6780  mapvalg  6827  ixpsnval  6870  ixpeq1  6878  snexxph  7149  fival  7169  acneq  7417  prplnqu  7840  cauappcvgprlemlim  7881  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgsr  8022  pitonnlem2  8067  pitonn  8068  recidpipr  8076  nntopi  8114  axcaucvglemval  8117  csbwrdg  11144  shftlem  11378  shftfibg  11382  shftdm  11384  shftfib  11385  negfi  11790  tgval  13347  ptex  13349  eqglact  13814  isghm  13832  ixpsnbasval  14483  plyval  15459  vtxdfifiun  16151