Theorem sbcbidv 3798

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  [wsbc 3743

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3744

This theorem is used by:  sbcbii  3799  csbeq2dv  3859  csbied  3888  2nreu  4408  opelopabsb  5513  opelopabgf  5524  opelopabf  5529  sbcfng  6702  sbcfg  6703  fmptsnd  7167  mpof1o2d  8119  frpoins3xpg  8134  frpoins3xp3g  8135  wrd2ind  14767  isomnd  20199  isorng  20975  islmod  20996  elmptrab  23995  f1od2  33075  indexa  38412  sdclem2  38421  sdclem1  38422  fdc  38424  sbcalf  38791  sbcexf  38792  hdmap1ffval  42597  hdmap1fval  42598  hdmapffval  42628  hdmapfval  42629  hgmapffval  42687  hgmapfval  42688  rexrabdioph  43549  rexfrabdioph  43550  2rexfrabdioph  43551  3rexfrabdioph  43552  4rexfrabdioph  43553  6rexfrabdioph  43554  7rexfrabdioph  43555  2sbc6g  45153  2sbc5g  45154  or2expropbilem1  47797