Theorem sbcbidv 3806

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3751

This theorem is referenced by:  sbcbii  3807  csbeq2dv  3866  csbied  3895  2nreu  4403  opelopabsb  5485  opelopabgf  5495  opelopabf  5500  sbcfng  6667  sbcfg  6668  fmptsnd  7125  frpoins3xpg  8096  frpoins3xp3g  8097  wrd2ind  14664  islmod  20746  elmptrab  23690  f1od2  32617  isomnd  32988  isorng  33250  indexa  37700  sdclem2  37709  sdclem1  37710  fdc  37712  sbcalf  38081  sbcexf  38082  hdmap1ffval  41762  hdmap1fval  41763  hdmapffval  41793  hdmapfval  41794  hgmapffval  41852  hgmapfval  41853  f1o2d2  42194  rexrabdioph  42755  rexfrabdioph  42756  2rexfrabdioph  42757  3rexfrabdioph  42758  4rexfrabdioph  42759  6rexfrabdioph  42760  7rexfrabdioph  42761  2sbc6g  44377  2sbc5g  44378  or2expropbilem1  47006