Theorem sbcbidv 3864

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 2741	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		sbcbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	sbceqbid 3811	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805

This theorem is referenced by:  sbcbii  3865  csbeq2dv  3928  csbied  3959  2nreu  4467  opelopabsb  5549  opelopabgf  5559  opelopabf  5564  sbcfng  6744  sbcfg  6745  fmptsnd  7203  frpoins3xpg  8181  frpoins3xp3g  8182  wrd2ind  14771  islmod  20884  elmptrab  23856  f1od2  32735  isomnd  33051  isorng  33294  indexa  37693  sdclem2  37702  sdclem1  37703  fdc  37705  sbcalf  38074  sbcexf  38075  hdmap1ffval  41752  hdmap1fval  41753  hdmapffval  41783  hdmapfval  41784  hgmapffval  41842  hgmapfval  41843  f1o2d2  42228  rexrabdioph  42750  rexfrabdioph  42751  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  2sbc6g  44384  2sbc5g  44385  or2expropbilem1  46947