Metamath Proof Explorer

Theorem mrsubvr

Description: The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubvr.v 
|- V = ( mVR ` T )
mrsubvr.r 
|- R = ( mREx ` T )
mrsubvr.s 
|- S = ( mRSubst ` T )
Assertion mrsubvr 
|- ( ( F : A --> R /\ A C_ V /\ X e. A ) -> ( ( S ` F ) ` <" X "> ) = ( F ` X ) )

Proof

Step Hyp Ref Expression
1 mrsubvr.v 
 |-  V = ( mVR ` T )
2 mrsubvr.r 
 |-  R = ( mREx ` T )
3 mrsubvr.s 
 |-  S = ( mRSubst ` T )
4 ssun2 
 |-  V C_ ( ( mCN ` T ) u. V )
5 simp2 
 |-  ( ( F : A --> R /\ A C_ V /\ X e. A ) -> A C_ V )
6 simp3 
 |-  ( ( F : A --> R /\ A C_ V /\ X e. A ) -> X e. A )
7 5 6 sseldd 
 |-  ( ( F : A --> R /\ A C_ V /\ X e. A ) -> X e. V )
8 4 7 sseldi 
 |-  ( ( F : A --> R /\ A C_ V /\ X e. A ) -> X e. ( ( mCN ` T ) u. V ) )
9 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
10 9 1 2 3 mrsubcv 
 |-  ( ( F : A --> R /\ A C_ V /\ X e. ( ( mCN ` T ) u. V ) ) -> ( ( S ` F ) ` <" X "> ) = if ( X e. A , ( F ` X ) , <" X "> ) )
11 8 10 syld3an3 
 |-  ( ( F : A --> R /\ A C_ V /\ X e. A ) -> ( ( S ` F ) ` <" X "> ) = if ( X e. A , ( F ` X ) , <" X "> ) )
12 iftrue 
 |-  ( X e. A -> if ( X e. A , ( F ` X ) , <" X "> ) = ( F ` X ) )
13 12 3ad2ant3 
 |-  ( ( F : A --> R /\ A C_ V /\ X e. A ) -> if ( X e. A , ( F ` X ) , <" X "> ) = ( F ` X ) )
14 11 13 eqtrd 
 |-  ( ( F : A --> R /\ A C_ V /\ X e. A ) -> ( ( S ` F ) ` <" X "> ) = ( F ` X ) )