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 
|- F/_ x A
csbhypf.2 
|- F/_ x C
csbhypf.3 
|- ( x = A -> B = C )
Assertion csbhypf 
|- ( y = A -> [_ y / x ]_ B = C )

Proof

Step Hyp Ref Expression
1 csbhypf.1 
 |-  F/_ x A
2 csbhypf.2 
 |-  F/_ x C
3 csbhypf.3 
 |-  ( x = A -> B = C )
4 1 nfeq2 
 |-  F/ x y = A
5 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
6 5 2 nfeq 
 |-  F/ x [_ y / x ]_ B = C
7 4 6 nfim 
 |-  F/ 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 )