Theorem sbcbidv 3770

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712

This theorem is referenced by:  sbcbii  3772  csbied  3866  2nreu  4372  opelopabsb  5436  opelopabgf  5446  opelopabf  5451  sbcfng  6581  sbcfg  6582  fmptsnd  7023  wrd2ind  14364  islmod  20042  elmptrab  22886  f1od2  30958  isomnd  31229  isorng  31400  frpoins3xpg  33714  frpoins3xp3g  33715  indexa  35818  sdclem2  35827  sdclem1  35828  fdc  35830  sbcalf  36199  sbcexf  36200  hdmap1ffval  39736  hdmap1fval  39737  hdmapffval  39767  hdmapfval  39768  hgmapffval  39826  hgmapfval  39827  rexrabdioph  40532  rexfrabdioph  40533  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  2sbc6g  41922  2sbc5g  41923  or2expropbilem1  44413