Description: Rewrite a function's support based with its range rather than the universal class. See also frnsuppeq . (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ffs2.1 | ⊢ 𝐶 = ( 𝐵 ∖ { 𝑍 } ) | |
Assertion | ffs2 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ 𝐶 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffs2.1 | ⊢ 𝐶 = ( 𝐵 ∖ { 𝑍 } ) | |
2 | frnsuppeq | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝐵 ∖ { 𝑍 } ) ) ) ) | |
3 | 2 | 3impia | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝐵 ∖ { 𝑍 } ) ) ) |
4 | 1 | imaeq2i | ⊢ ( ◡ 𝐹 “ 𝐶 ) = ( ◡ 𝐹 “ ( 𝐵 ∖ { 𝑍 } ) ) |
5 | 3 4 | eqtr4di | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ 𝐶 ) ) |