Theorem sbcbidv 3751

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 1890	. 2 ⊢ Ⅎ𝑥𝜑
2		sbcbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	sbcbid 3750	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))

Syntax hints:   → wi 4   ↔ wb 207  [wsbc 3701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-sbc 3702

This theorem is referenced by:  sbcbii  3752  2nreu  4301  opelopabsb  5299  opelopabgf  5309  opelopabf  5314  sbcfng  6371  sbcfg  6372  fmptsnd  6785  wrd2ind  13909  islmod  19316  elmptrab  22107  f1od2  30118  isomnd  30332  isorng  30481  indexa  34486  sdclem2  34495  sdclem1  34496  fdc  34498  sbcalf  34872  sbcexf  34873  hdmap1ffval  38412  hdmap1fval  38413  hdmapffval  38443  hdmapfval  38444  hgmapffval  38502  hgmapfval  38503  rexrabdioph  38827  rexfrabdioph  38828  2rexfrabdioph  38829  3rexfrabdioph  38830  4rexfrabdioph  38831  6rexfrabdioph  38832  7rexfrabdioph  38833  2sbc6g  40237  2sbc5g  40238  or2expropbilem1  42737