Theorem sbcbidv 3796

Description: Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.) Drop ax-12 2184. (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 2737	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		sbcbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	sbceqbid 3747	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3741

This theorem is referenced by:  sbcbii  3797  csbeq2dv  3856  csbied  3885  2nreu  4396  opelopabsb  5478  opelopabgf  5488  opelopabf  5493  sbcfng  6659  sbcfg  6660  fmptsnd  7115  frpoins3xpg  8082  frpoins3xp3g  8083  wrd2ind  14648  isomnd  20054  isorng  20796  islmod  20817  elmptrab  23773  f1od2  32800  indexa  37936  sdclem2  37945  sdclem1  37946  fdc  37948  sbcalf  38317  sbcexf  38318  hdmap1ffval  42077  hdmap1fval  42078  hdmapffval  42108  hdmapfval  42109  hgmapffval  42167  hgmapfval  42168  f1o2d2  42511  rexrabdioph  43057  rexfrabdioph  43058  2rexfrabdioph  43059  3rexfrabdioph  43060  4rexfrabdioph  43061  6rexfrabdioph  43062  7rexfrabdioph  43063  2sbc6g  44677  2sbc5g  44678  or2expropbilem1  47299