Metamath Proof Explorer

Theorem fvsetsid

Description: The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018)

Ref Expression
Assertion fvsetsid 
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( F sSet <. X , Y >. ) ` X ) = Y )

Proof

Step Hyp Ref Expression
1 setsval 
 |-  ( ( F e. V /\ Y e. U ) -> ( F sSet <. X , Y >. ) = ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) )
2 1 3adant2 
 |-  ( ( F e. V /\ X e. W /\ Y e. U ) -> ( F sSet <. X , Y >. ) = ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) )
3 2 fveq1d 
 |-  ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( F sSet <. X , Y >. ) ` X ) = ( ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) ` X ) )
4 simp2 
 |-  ( ( F e. V /\ X e. W /\ Y e. U ) -> X e. W )
5 simp3 
 |-  ( ( F e. V /\ X e. W /\ Y e. U ) -> Y e. U )
6 neldifsn 
 |-  -. X e. ( _V \ { X } )
7 dmres 
 |-  dom ( F |` ( _V \ { X } ) ) = ( ( _V \ { X } ) i^i dom F )
8 inss1 
 |-  ( ( _V \ { X } ) i^i dom F ) C_ ( _V \ { X } )
9 7 8 eqsstri 
 |-  dom ( F |` ( _V \ { X } ) ) C_ ( _V \ { X } )
10 9 sseli 
 |-  ( X e. dom ( F |` ( _V \ { X } ) ) -> X e. ( _V \ { X } ) )
11 6 10 mto 
 |-  -. X e. dom ( F |` ( _V \ { X } ) )
12 11 a1i 
 |-  ( ( F e. V /\ X e. W /\ Y e. U ) -> -. X e. dom ( F |` ( _V \ { X } ) ) )
13 fsnunfv 
 |-  ( ( X e. W /\ Y e. U /\ -. X e. dom ( F |` ( _V \ { X } ) ) ) -> ( ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) ` X ) = Y )
14 4 5 12 13 syl3anc 
 |-  ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) ` X ) = Y )
15 3 14 eqtrd 
 |-  ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( F sSet <. X , Y >. ) ` X ) = Y )