Theorem sbcbidv 3631

Description: Formula-building deduction rule for class substitution. (Contributed by NM, 29-Dec-2014.)

Hypothesis

Ref	Expression
sbcbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
sbcbidv	⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem sbcbidv

Step	Hyp	Ref	Expression
1		nfv 1992	. 2 ⊢ Ⅎ𝑥𝜑
2		sbcbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	sbcbid 3630	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

Syntax hints:   → wi 4   ↔ wb 196  [wsbc 3576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-sbc 3577

This theorem is referenced by:  sbcbii  3632  opelopabsb  5135  opelopabgf  5145  opelopabf  5150  sbcfng  6203  sbcfg  6204  fmptsnd  6600  wrd2ind  13697  islmod  19089  elmptrab  21852  f1od2  29829  isomnd  30031  isorng  30129  indexa  33859  sdclem2  33869  sdclem1  33870  fdc  33872  sbcalf  34248  sbcexf  34249  hdmap1ffval  37605  hdmap1fval  37606  hdmapffval  37638  hdmapfval  37639  hgmapffval  37697  hgmapfval  37698  rexrabdioph  37878  rexfrabdioph  37879  2rexfrabdioph  37880  3rexfrabdioph  37881  4rexfrabdioph  37882  6rexfrabdioph  37883  7rexfrabdioph  37884  2sbc6g  39136  2sbc5g  39137