Theorem csbhypf 3883

Description: Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3516 for class substitution version. (Contributed by NM, 19-Dec-2008.)

Hypotheses

Ref	Expression
csbhypf.1	⊢ Ⅎ𝑥𝐴
csbhypf.2	⊢ Ⅎ𝑥𝐶
csbhypf.3	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)

Assertion

Ref	Expression
csbhypf	⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem csbhypf

Step	Hyp	Ref	Expression
1		csbhypf.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	nfeq2 2944	. . 3 ⊢ Ⅎ𝑥 𝑦 = 𝐴
3		nfcsb1v 3879	. . . 4 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
4		csbhypf.2	. . . 4 ⊢ Ⅎ𝑥𝐶
5	3, 4	nfeq 2940	. . 3 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 = 𝐶
6	2, 5	nfim 1919	. 2 ⊢ Ⅎ𝑥(𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)
7		eqeq1 2769	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴))
8		csbeq1a 3869	. . . 4 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
9	8	eqeq1d 2767	. . 3 ⊢ (𝑥 = 𝑦 → (𝐵 = 𝐶 ↔ ⦋𝑦 / 𝑥⦌𝐵 = 𝐶))
10	7, 9	imbi12d 347	. 2 ⊢ (𝑥 = 𝑦 → ((𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)))
11		csbhypf.3	. 2 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
12	6, 10, 11	chvarfv 2278	1 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1563  Ⅎwnfc 2912  ⦋csb 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-sbc 3748  df-csb 3856

This theorem is referenced by:  disji2  5089  disjprg  5101  disjxun  5103  tfisi  7843  coe1fzgsumdlem  22424  evl1gsumdlem  22477  iundisj2  25669  disji2f  32832  disjif2  32836  iundisj2f  32845  iundisj2fi  33054  evl1gprodd  42746