This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbhypf

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

Ref Expression
Hypotheses csbhypf.1 ⊢ Ⅎ _ x A
csbhypf.2 ⊢ Ⅎ _ x C
csbhypf.3 ⊢ x = A → B = C
Assertion csbhypf ⊢ y = A → ⦋ y / x⦌ B = C

Proof

Step Hyp Ref Expression
1 csbhypf.1 ⊢ Ⅎ _ x A
2 csbhypf.2 ⊢ Ⅎ _ x C
3 csbhypf.3 ⊢ x = A → B = C
4 1 nfeq2 ⊢ Ⅎ x y = A
5 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ B
6 5 2 nfeq ⊢ Ⅎ x ⦋ y / x⦌ B = C
7 4 6 nfim ⊢ Ⅎ x y = A → ⦋ y / x⦌ B = C
8 eqeq1 ⊢ x = y → x = A ↔ y = A
9 csbeq1a ⊢ x = y → B = ⦋ y / x⦌ B
10 9 eqeq1d ⊢ x = y → B = C ↔ ⦋ y / x⦌ B = C
11 8 10 imbi12d ⊢ x = y → x = A → B = C ↔ y = A → ⦋ y / x⦌ B = C
12 7 11 3 chvarfv ⊢ y = A → ⦋ y / x⦌ B = C