Theorem sbcbidv 3809

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3754

This theorem is referenced by:  sbcbii  3810  csbeq2dv  3869  csbied  3898  2nreu  4407  opelopabsb  5490  opelopabgf  5500  opelopabf  5505  sbcfng  6685  sbcfg  6686  fmptsnd  7143  frpoins3xpg  8119  frpoins3xp3g  8120  wrd2ind  14688  islmod  20770  elmptrab  23714  f1od2  32644  isomnd  33015  isorng  33277  indexa  37727  sdclem2  37736  sdclem1  37737  fdc  37739  sbcalf  38108  sbcexf  38109  hdmap1ffval  41789  hdmap1fval  41790  hdmapffval  41820  hdmapfval  41821  hgmapffval  41879  hgmapfval  41880  f1o2d2  42221  rexrabdioph  42782  rexfrabdioph  42783  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  2sbc6g  44404  2sbc5g  44405  or2expropbilem1  47033