Theorem sbcbidv 3785

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

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

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-sbc 3727

This theorem is referenced by:  sbcbii  3786  csbied  3880  2nreu  4387  opelopabsb  5468  opelopabgf  5478  opelopabf  5483  sbcfng  6642  sbcfg  6643  fmptsnd  7091  wrd2ind  14526  islmod  20225  elmptrab  23076  f1od2  31284  isomnd  31555  isorng  31739  frpoins3xpg  34013  frpoins3xp3g  34014  indexa  35989  sdclem2  35998  sdclem1  35999  fdc  36001  sbcalf  36370  sbcexf  36371  hdmap1ffval  40056  hdmap1fval  40057  hdmapffval  40087  hdmapfval  40088  hgmapffval  40146  hgmapfval  40147  rexrabdioph  40866  rexfrabdioph  40867  2rexfrabdioph  40868  3rexfrabdioph  40869  4rexfrabdioph  40870  6rexfrabdioph  40871  7rexfrabdioph  40872  2sbc6g  42343  2sbc5g  42344  or2expropbilem1  44866