Theorem sbcbidv 3801

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

Syntax hints:   → wi 4   ↔ wb 208  [wsbc 3746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-sbc 3747

This theorem is referenced by:  sbcbii  3802  csbeq2dv  3861  csbied  3890  2nreu  4400  opelopabsb  5502  opelopabgf  5513  opelopabf  5518  sbcfng  6690  sbcfg  6691  fmptsnd  7155  mpof1o2d  8107  frpoins3xpg  8122  frpoins3xp3g  8123  wrd2ind  14738  isomnd  20165  isorng  20912  islmod  20933  elmptrab  23889  f1od2  32923  indexa  38237  sdclem2  38246  sdclem1  38247  fdc  38249  sbcalf  38618  sbcexf  38619  hdmap1ffval  42424  hdmap1fval  42425  hdmapffval  42455  hdmapfval  42456  hgmapffval  42514  hgmapfval  42515  rexrabdioph  43376  rexfrabdioph  43377  2rexfrabdioph  43378  3rexfrabdioph  43379  4rexfrabdioph  43380  6rexfrabdioph  43381  7rexfrabdioph  43382  2sbc6g  44996  2sbc5g  44997  or2expropbilem1  47631