Theorem abbidv 2311

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364  {cab 2179

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186

This theorem is referenced by:  rabbidva2  2747  cdeqab  2975  sbceqbid  2992  csbeq1  3083  sbcel12g  3095  sbceqg  3096  csbeq2  3104  csbeq2d  3105  csbnestgf  3133  csbprc  3492  ifbi  3577  pweq  3604  sneq  3629  csbsng  3679  rabsn  3685  dfopg  3802  opeq1  3804  opeq2  3805  csbunig  3843  unieq  3844  inteq  3873  iineq1  3926  iineq2  3929  dfiin2g  3945  iinrabm  3975  iinxprg  3987  opabbid  4094  dcextest  4613  csbxpg  4740  csbdmg  4856  imasng  5030  csbrng  5127  iotaeq  5223  iotabi  5224  dfimafn  5605  fnsnfv  5616  fndmin  5665  fliftf  5842  oprabbid  5971  recseq  6359  freceq1  6445  freceq2  6446  frec0g  6450  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  qseq1  6637  qseq2  6638  qsinxp  6665  mapvalg  6712  ixpsnval  6755  ixpeq1  6763  snexxph  7009  fival  7029  prplnqu  7680  cauappcvgprlemlim  7721  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnkeqj  7750  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  caucvgprprlem1  7769  caucvgprprlem2  7770  caucvgsr  7862  pitonnlem2  7907  pitonn  7908  recidpipr  7916  nntopi  7954  axcaucvglemval  7957  csbwrdg  10943  shftlem  10960  shftfibg  10964  shftdm  10966  shftfib  10967  negfi  11371  tgval  12873  ptex  12875  eqglact  13295  isghm  13313  ixpsnbasval  13962  plyval  14878