Theorem sbcbidv 3784

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3729

This theorem is referenced by:  sbcbii  3785  csbeq2dv  3844  csbied  3873  2nreu  4384  opelopabsb  5485  opelopabgf  5495  opelopabf  5500  sbcfng  6665  sbcfg  6666  fmptsnd  7124  frpoins3xpg  8090  frpoins3xp3g  8091  wrd2ind  14685  isomnd  20098  isorng  20838  islmod  20859  elmptrab  23792  f1od2  32792  indexa  38054  sdclem2  38063  sdclem1  38064  fdc  38066  sbcalf  38435  sbcexf  38436  hdmap1ffval  42241  hdmap1fval  42242  hdmapffval  42272  hdmapfval  42273  hgmapffval  42331  hgmapfval  42332  f1o2d2  42674  rexrabdioph  43222  rexfrabdioph  43223  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  2sbc6g  44842  2sbc5g  44843  or2expropbilem1  47480