Theorem sbcbidv 3798

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

Syntax hints:   → wi 4   ↔ wb 209  [wsbc 3743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3744

This theorem is referenced by:  sbcbii  3799  csbeq2dv  3859  csbied  3888  2nreu  4408  opelopabsb  5514  opelopabgf  5525  opelopabf  5530  sbcfng  6702  sbcfg  6703  fmptsnd  7167  mpof1o2d  8120  frpoins3xpg  8135  frpoins3xp3g  8136  wrd2ind  14759  isomnd  20192  isorng  20943  islmod  20964  elmptrab  23963  f1od2  33030  indexa  38328  sdclem2  38337  sdclem1  38338  fdc  38340  sbcalf  38709  sbcexf  38710  hdmap1ffval  42515  hdmap1fval  42516  hdmapffval  42546  hdmapfval  42547  hgmapffval  42605  hgmapfval  42606  rexrabdioph  43469  rexfrabdioph  43470  2rexfrabdioph  43471  3rexfrabdioph  43472  4rexfrabdioph  43473  6rexfrabdioph  43474  7rexfrabdioph  43475  2sbc6g  45073  2sbc5g  45074  or2expropbilem1  47714