Theorem sbcbidv 3793

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739

This theorem is used by:  sbcbii  3794  csbeq2dv  3853  csbied  3882  2nreu  4401  opelopabsb  5500  opelopabgf  5511  opelopabf  5516  sbcfng  6694  sbcfg  6695  fmptsnd  7162  mpof1o2d  8120  frpoins3xpg  8135  frpoins3xp3g  8136  wrd2ind  14839  isomnd  20298  isorng  21079  islmod  21100  elmptrab  24107  f1od2  33244  indexa  38587  sdclem2  38596  sdclem1  38597  fdc  38599  sbcalf  38966  sbcexf  38967  hdmap1ffval  42772  hdmap1fval  42773  hdmapffval  42803  hdmapfval  42804  hgmapffval  42862  hgmapfval  42863  rexrabdioph  43739  rexfrabdioph  43740  2rexfrabdioph  43741  3rexfrabdioph  43742  4rexfrabdioph  43743  6rexfrabdioph  43744  7rexfrabdioph  43745  2sbc6g  45343  2sbc5g  45344  or2expropbilem1  48024