Theorem sbcbidv 3837

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

Syntax hints:   → wi 4   ↔ wb 205  [wsbc 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779

This theorem is referenced by:  sbcbii  3838  csbied  3932  2nreu  4442  opelopabsb  5531  opelopabgf  5541  opelopabf  5546  sbcfng  6715  sbcfg  6716  fmptsnd  7167  frpoins3xpg  8126  frpoins3xp3g  8127  wrd2ind  14673  islmod  20475  elmptrab  23331  f1od2  31946  isomnd  32219  isorng  32417  indexa  36601  sdclem2  36610  sdclem1  36611  fdc  36613  sbcalf  36982  sbcexf  36983  hdmap1ffval  40666  hdmap1fval  40667  hdmapffval  40697  hdmapfval  40698  hgmapffval  40756  hgmapfval  40757  f1o2d2  41055  rexrabdioph  41532  rexfrabdioph  41533  2rexfrabdioph  41534  3rexfrabdioph  41535  4rexfrabdioph  41536  6rexfrabdioph  41537  7rexfrabdioph  41538  2sbc6g  43174  2sbc5g  43175  or2expropbilem1  45742