Theorem sbcbidv 3753

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

Syntax hints:   → wi 4   ↔ wb 209  [wsbc 3694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3695

This theorem is referenced by:  sbcbii  3755  csbied  3849  2nreu  4356  opelopabsb  5411  opelopabgf  5421  opelopabf  5426  sbcfng  6542  sbcfg  6543  fmptsnd  6984  wrd2ind  14288  islmod  19903  elmptrab  22724  f1od2  30776  isomnd  31046  isorng  31217  frpoins3xpg  33524  frpoins3xp3g  33525  indexa  35628  sdclem2  35637  sdclem1  35638  fdc  35640  sbcalf  36009  sbcexf  36010  hdmap1ffval  39546  hdmap1fval  39547  hdmapffval  39577  hdmapfval  39578  hgmapffval  39636  hgmapfval  39637  rexrabdioph  40319  rexfrabdioph  40320  2rexfrabdioph  40321  3rexfrabdioph  40322  4rexfrabdioph  40323  6rexfrabdioph  40324  7rexfrabdioph  40325  2sbc6g  41706  2sbc5g  41707  or2expropbilem1  44198