Theorem sbcbidv 3798

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 2738	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		sbcbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	sbceqbid 3749	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3743

This theorem is referenced by:  sbcbii  3799  csbeq2dv  3858  csbied  3887  2nreu  4398  opelopabsb  5488  opelopabgf  5498  opelopabf  5503  sbcfng  6669  sbcfg  6670  fmptsnd  7127  frpoins3xpg  8094  frpoins3xp3g  8095  wrd2ind  14660  isomnd  20069  isorng  20811  islmod  20832  elmptrab  23788  f1od2  32815  indexa  38013  sdclem2  38022  sdclem1  38023  fdc  38025  sbcalf  38394  sbcexf  38395  hdmap1ffval  42200  hdmap1fval  42201  hdmapffval  42231  hdmapfval  42232  hgmapffval  42290  hgmapfval  42291  f1o2d2  42634  rexrabdioph  43180  rexfrabdioph  43181  2rexfrabdioph  43182  3rexfrabdioph  43183  4rexfrabdioph  43184  6rexfrabdioph  43185  7rexfrabdioph  43186  2sbc6g  44800  2sbc5g  44801  or2expropbilem1  47421