Theorem sbcbidv 3798

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 3749	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

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

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 3743

This theorem is referenced by:  sbcbii  3799  csbeq2dv  3858  csbied  3887  2nreu  4395  opelopabsb  5473  opelopabgf  5483  opelopabf  5488  sbcfng  6649  sbcfg  6650  fmptsnd  7105  frpoins3xpg  8073  frpoins3xp3g  8074  wrd2ind  14629  isomnd  20002  isorng  20746  islmod  20767  elmptrab  23712  f1od2  32663  indexa  37713  sdclem2  37722  sdclem1  37723  fdc  37725  sbcalf  38094  sbcexf  38095  hdmap1ffval  41774  hdmap1fval  41775  hdmapffval  41805  hdmapfval  41806  hgmapffval  41864  hgmapfval  41865  f1o2d2  42206  rexrabdioph  42767  rexfrabdioph  42768  2rexfrabdioph  42769  3rexfrabdioph  42770  4rexfrabdioph  42771  6rexfrabdioph  42772  7rexfrabdioph  42773  2sbc6g  44388  2sbc5g  44389  or2expropbilem1  47016