Theorem sbcbidv 3792

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

Syntax hints:   → wi 4   ↔ wb 206  [wsbc 3736

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sbc 3737

This theorem is referenced by:  sbcbii  3793  csbeq2dv  3852  csbied  3881  2nreu  4391  opelopabsb  5468  opelopabgf  5478  opelopabf  5483  sbcfng  6648  sbcfg  6649  fmptsnd  7103  frpoins3xpg  8070  frpoins3xp3g  8071  wrd2ind  14630  isomnd  20035  isorng  20776  islmod  20797  elmptrab  23742  f1od2  32702  indexa  37781  sdclem2  37790  sdclem1  37791  fdc  37793  sbcalf  38162  sbcexf  38163  hdmap1ffval  41842  hdmap1fval  41843  hdmapffval  41873  hdmapfval  41874  hgmapffval  41932  hgmapfval  41933  f1o2d2  42274  rexrabdioph  42835  rexfrabdioph  42836  2rexfrabdioph  42837  3rexfrabdioph  42838  4rexfrabdioph  42839  6rexfrabdioph  42840  7rexfrabdioph  42841  2sbc6g  44456  2sbc5g  44457  or2expropbilem1  47071