Theorem csbhypf 3866

Description: Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3493 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 2919	. . 3 ⊢ Ⅎ𝑥 𝑦 = 𝐴
3		nfcsb1v 3862	. . . 4 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
4		csbhypf.2	. . . 4 ⊢ Ⅎ𝑥𝐶
5	3, 4	nfeq 2915	. . 3 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 = 𝐶
6	2, 5	nfim 1903	. 2 ⊢ Ⅎ𝑥(𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)
7		eqeq1 2744	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴))
8		csbeq1a 3852	. . . 4 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
9	8	eqeq1d 2742	. . 3 ⊢ (𝑥 = 𝑦 → (𝐵 = 𝐶 ↔ ⦋𝑦 / 𝑥⦌𝐵 = 𝐶))
10	7, 9	imbi12d 345	. 2 ⊢ (𝑥 = 𝑦 → ((𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)))
11		csbhypf.3	. 2 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
12	6, 10, 11	chvarfv 2252	1 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1547  Ⅎwnfc 2887  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-sbc 3731  df-csb 3839

This theorem is referenced by:  disji2  5063  disjprg  5075  disjxun  5077  tfisi  7806  coe1fzgsumdlem  22296  evl1gsumdlem  22349  iundisj2  25541  disji2f  32673  disjif2  32677  iundisj2f  32686  iundisj2fi  32896  evl1gprodd  42603