Metamath Proof Explorer


Theorem elsuppfn

Description: An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019)

Ref Expression
Assertion elsuppfn ( ( 𝐹 Fn 𝑋𝑋𝑉𝑍𝑊 ) → ( 𝑆 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑆𝑋 ∧ ( 𝐹𝑆 ) ≠ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 suppvalfn ( ( 𝐹 Fn 𝑋𝑋𝑉𝑍𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑖𝑋 ∣ ( 𝐹𝑖 ) ≠ 𝑍 } )
2 1 eleq2d ( ( 𝐹 Fn 𝑋𝑋𝑉𝑍𝑊 ) → ( 𝑆 ∈ ( 𝐹 supp 𝑍 ) ↔ 𝑆 ∈ { 𝑖𝑋 ∣ ( 𝐹𝑖 ) ≠ 𝑍 } ) )
3 fveq2 ( 𝑖 = 𝑆 → ( 𝐹𝑖 ) = ( 𝐹𝑆 ) )
4 3 neeq1d ( 𝑖 = 𝑆 → ( ( 𝐹𝑖 ) ≠ 𝑍 ↔ ( 𝐹𝑆 ) ≠ 𝑍 ) )
5 4 elrab ( 𝑆 ∈ { 𝑖𝑋 ∣ ( 𝐹𝑖 ) ≠ 𝑍 } ↔ ( 𝑆𝑋 ∧ ( 𝐹𝑆 ) ≠ 𝑍 ) )
6 2 5 bitrdi ( ( 𝐹 Fn 𝑋𝑋𝑉𝑍𝑊 ) → ( 𝑆 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑆𝑋 ∧ ( 𝐹𝑆 ) ≠ 𝑍 ) ) )