Theorem sbcbidv 3829

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-sbc 3775

This theorem is referenced by:  sbcbii  3831  2nreu  4395  opelopabsb  5419  opelopabgf  5429  opelopabf  5434  sbcfng  6513  sbcfg  6514  fmptsnd  6933  wrd2ind  14087  islmod  19640  elmptrab  22437  f1od2  30459  isomnd  30704  isorng  30874  indexa  35010  sdclem2  35019  sdclem1  35020  fdc  35022  sbcalf  35394  sbcexf  35395  hdmap1ffval  38933  hdmap1fval  38934  hdmapffval  38964  hdmapfval  38965  hgmapffval  39023  hgmapfval  39024  rexrabdioph  39398  rexfrabdioph  39399  2rexfrabdioph  39400  3rexfrabdioph  39401  4rexfrabdioph  39402  6rexfrabdioph  39403  7rexfrabdioph  39404  2sbc6g  40754  2sbc5g  40755  or2expropbilem1  43274