Theorem sbcbidv 3688

Description: Formula-building deduction 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 2010	. 2 ⊢ Ⅎ𝑥𝜑
2		sbcbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	sbcbid 3687	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

Syntax hints:   → wi 4   ↔ wb 198  [wsbc 3633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-sbc 3634

This theorem is referenced by:  sbcbii  3689  opelopabsb  5181  opelopabgf  5191  opelopabf  5196  sbcfng  6253  sbcfg  6254  fmptsnd  6664  wrd2ind  13778  wrd2indOLD  13779  islmod  19185  elmptrab  21959  f1od2  30017  isomnd  30217  isorng  30315  indexa  34016  sdclem2  34025  sdclem1  34026  fdc  34028  sbcalf  34404  sbcexf  34405  hdmap1ffval  37816  hdmap1fval  37817  hdmapffval  37847  hdmapfval  37848  hgmapffval  37906  hgmapfval  37907  rexrabdioph  38144  rexfrabdioph  38145  2rexfrabdioph  38146  3rexfrabdioph  38147  4rexfrabdioph  38148  6rexfrabdioph  38149  7rexfrabdioph  38150  2sbc6g  39397  2sbc5g  39398