Theorem sbcbidv 3794

Description: Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.) Drop ax-12 2182. (Revised by GG, 1-Dec-2023.)

Hypothesis

Ref	Expression
sbcbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
sbcbidv	⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem sbcbidv

Step	Hyp	Ref	Expression
1		eqidd 2735	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		sbcbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	sbceqbid 3745	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

Syntax hints:   → wi 4   ↔ wb 206  [wsbc 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-sbc 3739

This theorem is referenced by:  sbcbii  3795  csbeq2dv  3854  csbied  3883  2nreu  4394  opelopabsb  5476  opelopabgf  5486  opelopabf  5491  sbcfng  6657  sbcfg  6658  fmptsnd  7113  frpoins3xpg  8080  frpoins3xp3g  8081  wrd2ind  14644  isomnd  20050  isorng  20792  islmod  20813  elmptrab  23769  f1od2  32747  indexa  37873  sdclem2  37882  sdclem1  37883  fdc  37885  sbcalf  38254  sbcexf  38255  hdmap1ffval  41994  hdmap1fval  41995  hdmapffval  42025  hdmapfval  42026  hgmapffval  42084  hgmapfval  42085  f1o2d2  42431  rexrabdioph  42978  rexfrabdioph  42979  2rexfrabdioph  42980  3rexfrabdioph  42981  4rexfrabdioph  42982  6rexfrabdioph  42983  7rexfrabdioph  42984  2sbc6g  44598  2sbc5g  44599  or2expropbilem1  47220