Theorem sbcbidv 3797

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sbc 3743

This theorem is used by:  sbcbii  3798  csbeq2dv  3858  csbied  3887  2nreu  4405  opelopabsb  5508  opelopabgf  5519  opelopabf  5524  sbcfng  6728  sbcfg  6729  fmptsnd  7197  f1od2  8135  mpof1o2d  8164  frpoins3xpg  8184  frpoins3xp3g  8185  wrd2ind  14900  isomnd  20367  isorng  21148  islmod  21169  elmptrab  24176  indexa  38859  sdclem2  38868  sdclem1  38869  fdc  38871  sbcalf  39238  sbcexf  39239  hdmap1ffval  43044  hdmap1fval  43045  hdmapffval  43075  hdmapfval  43076  hgmapffval  43134  hgmapfval  43135  rexrabdioph  43994  rexfrabdioph  43995  2rexfrabdioph  43996  3rexfrabdioph  43997  4rexfrabdioph  43998  6rexfrabdioph  43999  7rexfrabdioph  44000  2sbc6g  45591  2sbc5g  45592  or2expropbilem1  48307