Theorem sbcbidv 3785

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730

This theorem is referenced by:  sbcbii  3786  csbeq2dv  3845  csbied  3874  2nreu  4385  opelopabsb  5480  opelopabgf  5490  opelopabf  5495  sbcfng  6661  sbcfg  6662  fmptsnd  7119  frpoins3xpg  8085  frpoins3xp3g  8086  wrd2ind  14680  isomnd  20093  isorng  20833  islmod  20854  elmptrab  23806  f1od2  32811  indexa  38074  sdclem2  38083  sdclem1  38084  fdc  38086  sbcalf  38455  sbcexf  38456  hdmap1ffval  42261  hdmap1fval  42262  hdmapffval  42292  hdmapfval  42293  hgmapffval  42351  hgmapfval  42352  f1o2d2  42694  rexrabdioph  43246  rexfrabdioph  43247  2rexfrabdioph  43248  3rexfrabdioph  43249  4rexfrabdioph  43250  6rexfrabdioph  43251  7rexfrabdioph  43252  2sbc6g  44866  2sbc5g  44867  or2expropbilem1  47498