Description: An element of the support of a function with a given domain. This version of elsuppfn assumes F is a set rather than its domain X , avoiding ax-rep . (Contributed by SN, 5-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | elsuppfng | ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑆 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑆 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑆 ) ≠ 𝑍 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | suppvalfng | ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑖 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } ) | |
2 | 1 | eleq2d | ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑆 ∈ ( 𝐹 supp 𝑍 ) ↔ 𝑆 ∈ { 𝑖 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } ) ) |
3 | fveq2 | ⊢ ( 𝑖 = 𝑆 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑆 ) ) | |
4 | 3 | neeq1d | ⊢ ( 𝑖 = 𝑆 → ( ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 ↔ ( 𝐹 ‘ 𝑆 ) ≠ 𝑍 ) ) |
5 | 4 | elrab | ⊢ ( 𝑆 ∈ { 𝑖 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } ↔ ( 𝑆 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑆 ) ≠ 𝑍 ) ) |
6 | 2 5 | bitrdi | ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑆 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑆 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑆 ) ≠ 𝑍 ) ) ) |