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  37772  sdclem2  37781  sdclem1  37782  fdc  37784  sbcalf  38153  sbcexf  38154  hdmap1ffval  41893  hdmap1fval  41894  hdmapffval  41924  hdmapfval  41925  hgmapffval  41983  hgmapfval  41984  f1o2d2  42325  rexrabdioph  42886  rexfrabdioph  42887  2rexfrabdioph  42888  3rexfrabdioph  42889  4rexfrabdioph  42890  6rexfrabdioph  42891  7rexfrabdioph  42892  2sbc6g  44507  2sbc5g  44508  or2expropbilem1  47131