Theorem sbcbidv 3836

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-sbc 3777

This theorem is referenced by:  sbcbii  3837  csbied  3930  2nreu  4446  opelopabsb  5536  opelopabgf  5546  opelopabf  5551  sbcfng  6725  sbcfg  6726  fmptsnd  7183  frpoins3xpg  8154  frpoins3xp3g  8155  wrd2ind  14731  islmod  20840  elmptrab  23822  f1od2  32635  isomnd  32936  isorng  33177  indexa  37434  sdclem2  37443  sdclem1  37444  fdc  37446  sbcalf  37815  sbcexf  37816  hdmap1ffval  41494  hdmap1fval  41495  hdmapffval  41525  hdmapfval  41526  hgmapffval  41584  hgmapfval  41585  f1o2d2  41957  rexrabdioph  42451  rexfrabdioph  42452  2rexfrabdioph  42453  3rexfrabdioph  42454  4rexfrabdioph  42455  6rexfrabdioph  42456  7rexfrabdioph  42457  2sbc6g  44089  2sbc5g  44090  or2expropbilem1  46647