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 | ⊢ ( 𝜑 → 𝐺 = ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) | |
| bj-fvsnun1.eldif | ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ∖ { 𝐴 } ) ) | ||
| Assertion | bj-fvsnun1 | ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐷 ) = ( 𝐹 ‘ 𝐷 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-fvsnun.un | ⊢ ( 𝜑 → 𝐺 = ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) | |
| 2 | bj-fvsnun1.eldif | ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ∖ { 𝐴 } ) ) | |
| 3 | eldifsnneq | ⊢ ( 𝐷 ∈ ( 𝐶 ∖ { 𝐴 } ) → ¬ 𝐷 = 𝐴 ) | |
| 4 | 2 3 | syl | ⊢ ( 𝜑 → ¬ 𝐷 = 𝐴 ) |
| 5 | 1 4 | bj-fununsn1 | ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐷 ) = ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ‘ 𝐷 ) ) |
| 6 | 2 | fvresd | ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ‘ 𝐷 ) = ( 𝐹 ‘ 𝐷 ) ) |
| 7 | 5 6 | eqtrd | ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐷 ) = ( 𝐹 ‘ 𝐷 ) ) |