Theorem sbcbidv 3794

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3740

This theorem is used by:  sbcbii  3795  csbeq2dv  3854  csbied  3883  2nreu  4402  opelopabsb  5508  opelopabgf  5519  opelopabf  5524  sbcfng  6700  sbcfg  6701  fmptsnd  7168  mpof1o2d  8124  frpoins3xpg  8139  frpoins3xp3g  8140  wrd2ind  14795  isomnd  20253  isorng  21030  islmod  21051  elmptrab  24056  f1od2  33193  indexa  38486  sdclem2  38495  sdclem1  38496  fdc  38498  sbcalf  38865  sbcexf  38866  hdmap1ffval  42671  hdmap1fval  42672  hdmapffval  42702  hdmapfval  42703  hgmapffval  42761  hgmapfval  42762  rexrabdioph  43638  rexfrabdioph  43639  2rexfrabdioph  43640  3rexfrabdioph  43641  4rexfrabdioph  43642  6rexfrabdioph  43643  7rexfrabdioph  43644  2sbc6g  45242  2sbc5g  45243  or2expropbilem1  47923