Description: The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. (Contributed by NM, 23-Sep-2007) Put in deduction form and remove two sethood hypotheses. (Revised by BJ, 18-Mar-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bj-fvsnun.un | |- ( ph -> G = ( ( F |` ( C \ { A } ) ) u. { <. A , B >. } ) ) |
|
| bj-fvsnun1.eldif | |- ( ph -> D e. ( C \ { A } ) ) |
||
| Assertion | bj-fvsnun1 | |- ( ph -> ( G ` D ) = ( F ` D ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-fvsnun.un | |- ( ph -> G = ( ( F |` ( C \ { A } ) ) u. { <. A , B >. } ) ) |
|
| 2 | bj-fvsnun1.eldif | |- ( ph -> D e. ( C \ { A } ) ) |
|
| 3 | eldifsnneq | |- ( D e. ( C \ { A } ) -> -. D = A ) |
|
| 4 | 2 3 | syl | |- ( ph -> -. D = A ) |
| 5 | 1 4 | bj-fununsn1 | |- ( ph -> ( G ` D ) = ( ( F |` ( C \ { A } ) ) ` D ) ) |
| 6 | 2 | fvresd | |- ( ph -> ( ( F |` ( C \ { A } ) ) ` D ) = ( F ` D ) ) |
| 7 | 5 6 | eqtrd | |- ( ph -> ( G ` D ) = ( F ` D ) ) |