Theorem sbcbidv 3793

Description: Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.) Drop ax-12 2212. (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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  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  5503  opelopabgf  5514  opelopabf  5519  sbcfng  6706  sbcfg  6707  fmptsnd  7174  mpof1o2d  8137  frpoins3xpg  8157  frpoins3xp3g  8158  wrd2ind  14872  isomnd  20337  isorng  21118  islmod  21139  elmptrab  24146  f1od2  33353  indexa  38710  sdclem2  38719  sdclem1  38720  fdc  38722  sbcalf  39089  sbcexf  39090  hdmap1ffval  42895  hdmap1fval  42896  hdmapffval  42926  hdmapfval  42927  hgmapffval  42985  hgmapfval  42986  rexrabdioph  43844  rexfrabdioph  43845  2rexfrabdioph  43846  3rexfrabdioph  43847  4rexfrabdioph  43848  6rexfrabdioph  43849  7rexfrabdioph  43850  2sbc6g  45442  2sbc5g  45443  or2expropbilem1  48145