Theorem sbcbidv 3826

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

Syntax hints:   → wi 4   ↔ wb 208  [wsbc 3771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3772

This theorem is referenced by:  sbcbii  3828  2nreu  4392  opelopabsb  5416  opelopabgf  5426  opelopabf  5431  sbcfng  6510  sbcfg  6511  fmptsnd  6930  wrd2ind  14084  islmod  19637  elmptrab  22434  f1od2  30456  isomnd  30702  isorng  30872  indexa  35007  sdclem2  35016  sdclem1  35017  fdc  35019  sbcalf  35391  sbcexf  35392  hdmap1ffval  38930  hdmap1fval  38931  hdmapffval  38961  hdmapfval  38962  hgmapffval  39020  hgmapfval  39021  rexrabdioph  39389  rexfrabdioph  39390  2rexfrabdioph  39391  3rexfrabdioph  39392  4rexfrabdioph  39393  6rexfrabdioph  39394  7rexfrabdioph  39395  2sbc6g  40745  2sbc5g  40746  or2expropbilem1  43266