Theorem sbcbidv 3812

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3757

This theorem is referenced by:  sbcbii  3813  csbeq2dv  3872  csbied  3901  2nreu  4410  opelopabsb  5493  opelopabgf  5503  opelopabf  5508  sbcfng  6688  sbcfg  6689  fmptsnd  7146  frpoins3xpg  8122  frpoins3xp3g  8123  wrd2ind  14695  islmod  20777  elmptrab  23721  f1od2  32651  isomnd  33022  isorng  33284  indexa  37734  sdclem2  37743  sdclem1  37744  fdc  37746  sbcalf  38115  sbcexf  38116  hdmap1ffval  41796  hdmap1fval  41797  hdmapffval  41827  hdmapfval  41828  hgmapffval  41886  hgmapfval  41887  f1o2d2  42228  rexrabdioph  42789  rexfrabdioph  42790  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  2sbc6g  44411  2sbc5g  44412  or2expropbilem1  47037