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 )