Metamath Proof Explorer


Theorem elsuppfng

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 𝑍 ) ↔ ( 𝑆𝑋 ∧ ( 𝐹𝑆 ) ≠ 𝑍 ) ) )

Proof

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 𝑍 ) ↔ ( 𝑆𝑋 ∧ ( 𝐹𝑆 ) ≠ 𝑍 ) ) )