Theorem sbcbidv 3845

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789

This theorem is referenced by:  sbcbii  3846  csbeq2dv  3906  csbied  3935  2nreu  4444  opelopabsb  5535  opelopabgf  5545  opelopabf  5550  sbcfng  6733  sbcfg  6734  fmptsnd  7189  frpoins3xpg  8165  frpoins3xp3g  8166  wrd2ind  14761  islmod  20862  elmptrab  23835  f1od2  32732  isomnd  33078  isorng  33329  indexa  37740  sdclem2  37749  sdclem1  37750  fdc  37752  sbcalf  38121  sbcexf  38122  hdmap1ffval  41797  hdmap1fval  41798  hdmapffval  41828  hdmapfval  41829  hgmapffval  41887  hgmapfval  41888  f1o2d2  42274  rexrabdioph  42805  rexfrabdioph  42806  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  2sbc6g  44434  2sbc5g  44435  or2expropbilem1  47044