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 ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → S ∈ supp Z⁡ F ↔ S ∈ X ∧ F ⁡ S ≠ Z

Proof

Step Hyp Ref Expression
1 suppvalfn ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → F supp Z = i ∈ X | F ⁡ i ≠ Z
2 1 eleq2d ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → S ∈ supp Z⁡ F ↔ S ∈ i ∈ X | F ⁡ i ≠ Z
3 fveq2 ⊢ i = S → F ⁡ i = F ⁡ S
4 3 neeq1d ⊢ i = S → F ⁡ i ≠ Z ↔ F ⁡ S ≠ Z
5 4 elrab ⊢ S ∈ i ∈ X | F ⁡ i ≠ Z ↔ S ∈ X ∧ F ⁡ S ≠ Z
6 2 5 bitrdi ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → S ∈ supp Z⁡ F ↔ S ∈ X ∧ F ⁡ S ≠ Z