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