Theorem sbcbidv 3775

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sbc 3717

This theorem is referenced by:  sbcbii  3776  csbied  3870  2nreu  4375  opelopabsb  5443  opelopabgf  5453  opelopabf  5458  sbcfng  6597  sbcfg  6598  fmptsnd  7041  wrd2ind  14436  islmod  20127  elmptrab  22978  f1od2  31056  isomnd  31327  isorng  31498  frpoins3xpg  33787  frpoins3xp3g  33788  indexa  35891  sdclem2  35900  sdclem1  35901  fdc  35903  sbcalf  36272  sbcexf  36273  hdmap1ffval  39809  hdmap1fval  39810  hdmapffval  39840  hdmapfval  39841  hgmapffval  39899  hgmapfval  39900  rexrabdioph  40616  rexfrabdioph  40617  2rexfrabdioph  40618  3rexfrabdioph  40619  4rexfrabdioph  40620  6rexfrabdioph  40621  7rexfrabdioph  40622  2sbc6g  42033  2sbc5g  42034  or2expropbilem1  44526