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  31977  isomnd  32250  isorng  32448  indexa  36649  sdclem2  36658  sdclem1  36659  fdc  36661  sbcalf  37030  sbcexf  37031  hdmap1ffval  40714  hdmap1fval  40715  hdmapffval  40745  hdmapfval  40746  hgmapffval  40804  hgmapfval  40805  f1o2d2  41103  rexrabdioph  41580  rexfrabdioph  41581  2rexfrabdioph  41582  3rexfrabdioph  41583  4rexfrabdioph  41584  6rexfrabdioph  41585  7rexfrabdioph  41586  2sbc6g  43222  2sbc5g  43223  or2expropbilem1  45790