Theorem sbcbidv 3797

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743

This theorem is used by:  sbcbii  3798  csbeq2dv  3857  csbied  3886  2nreu  4405  opelopabsb  5512  opelopabgf  5523  opelopabf  5528  sbcfng  6703  sbcfg  6704  fmptsnd  7170  mpof1o2d  8126  frpoins3xpg  8141  frpoins3xp3g  8142  wrd2ind  14794  isomnd  20251  isorng  21028  islmod  21049  elmptrab  24054  f1od2  33177  indexa  38470  sdclem2  38479  sdclem1  38480  fdc  38482  sbcalf  38849  sbcexf  38850  hdmap1ffval  42655  hdmap1fval  42656  hdmapffval  42686  hdmapfval  42687  hgmapffval  42745  hgmapfval  42746  rexrabdioph  43622  rexfrabdioph  43623  2rexfrabdioph  43624  3rexfrabdioph  43625  4rexfrabdioph  43626  6rexfrabdioph  43627  7rexfrabdioph  43628  2sbc6g  45226  2sbc5g  45227  or2expropbilem1  47907