Theorem sbcbidv 3851

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792

This theorem is referenced by:  sbcbii  3852  csbeq2dv  3915  csbied  3946  2nreu  4450  opelopabsb  5540  opelopabgf  5550  opelopabf  5555  sbcfng  6734  sbcfg  6735  fmptsnd  7189  frpoins3xpg  8164  frpoins3xp3g  8165  wrd2ind  14758  islmod  20879  elmptrab  23851  f1od2  32739  isomnd  33061  isorng  33309  indexa  37720  sdclem2  37729  sdclem1  37730  fdc  37732  sbcalf  38101  sbcexf  38102  hdmap1ffval  41778  hdmap1fval  41779  hdmapffval  41809  hdmapfval  41810  hgmapffval  41868  hgmapfval  41869  f1o2d2  42253  rexrabdioph  42782  rexfrabdioph  42783  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  2sbc6g  44411  2sbc5g  44412  or2expropbilem1  46982