Theorem sbcbidv 3821

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766

This theorem is referenced by:  sbcbii  3822  csbeq2dv  3881  csbied  3910  2nreu  4419  opelopabsb  5505  opelopabgf  5515  opelopabf  5520  sbcfng  6703  sbcfg  6704  fmptsnd  7161  frpoins3xpg  8139  frpoins3xp3g  8140  wrd2ind  14741  islmod  20821  elmptrab  23765  f1od2  32698  isomnd  33069  isorng  33321  indexa  37757  sdclem2  37766  sdclem1  37767  fdc  37769  sbcalf  38138  sbcexf  38139  hdmap1ffval  41814  hdmap1fval  41815  hdmapffval  41845  hdmapfval  41846  hgmapffval  41904  hgmapfval  41905  f1o2d2  42284  rexrabdioph  42817  rexfrabdioph  42818  2rexfrabdioph  42819  3rexfrabdioph  42820  4rexfrabdioph  42821  6rexfrabdioph  42822  7rexfrabdioph  42823  2sbc6g  44439  2sbc5g  44440  or2expropbilem1  47061