Theorem sbcbidv 3780

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

Syntax hints:   → wi 4   ↔ wb 208  [wsbc 3725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-sbc 3726

This theorem is referenced by:  sbcbii  3781  csbeq2dv  3840  csbied  3869  2nreu  4375  opelopabsb  5475  opelopabgf  5485  opelopabf  5490  sbcfng  6656  sbcfg  6657  fmptsnd  7117  mpof1o2d  8069  frpoins3xpg  8084  frpoins3xp3g  8085  wrd2ind  14680  isomnd  20093  isorng  20837  islmod  20858  elmptrab  23814  f1od2  32815  indexa  38115  sdclem2  38124  sdclem1  38125  fdc  38127  sbcalf  38496  sbcexf  38497  hdmap1ffval  42302  hdmap1fval  42303  hdmapffval  42333  hdmapfval  42334  hgmapffval  42392  hgmapfval  42393  rexrabdioph  43254  rexfrabdioph  43255  2rexfrabdioph  43256  3rexfrabdioph  43257  4rexfrabdioph  43258  6rexfrabdioph  43259  7rexfrabdioph  43260  2sbc6g  44874  2sbc5g  44875  or2expropbilem1  47509