This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dffn5f

Description: Representation of a function in terms of its values. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypothesis dffn5f.1 ⊢ Ⅎ _ x F
Assertion dffn5f ⊢ F Fn A ↔ F = x ∈ A ⟼ F ⁡ x

Proof

Step Hyp Ref Expression
1 dffn5f.1 ⊢ Ⅎ _ x F
2 dffn5 ⊢ F Fn A ↔ F = z ∈ A ⟼ F ⁡ z
3 nfcv ⊢ Ⅎ _ x z
4 1 3 nffv ⊢ Ⅎ _ x F ⁡ z
5 nfcv ⊢ Ⅎ _ z F ⁡ x
6 fveq2 ⊢ z = x → F ⁡ z = F ⁡ x
7 4 5 6 cbvmpt ⊢ z ∈ A ⟼ F ⁡ z = x ∈ A ⟼ F ⁡ x
8 7 eqeq2i ⊢ F = z ∈ A ⟼ F ⁡ z ↔ F = x ∈ A ⟼ F ⁡ x
9 2 8 bitri ⊢ F Fn A ↔ F = x ∈ A ⟼ F ⁡ x