Metamath Proof Explorer

Theorem ffnfvf

Description: A function maps to a class to which all values belong. This version of ffnfv uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006)

Ref Expression
Hypotheses ffnfvf.1 ⊢ Ⅎ _ x A
ffnfvf.2 ⊢ Ⅎ _ x B
ffnfvf.3 ⊢ Ⅎ _ x F
Assertion ffnfvf ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 ffnfvf.1 ⊢ Ⅎ _ x A
2 ffnfvf.2 ⊢ Ⅎ _ x B
3 ffnfvf.3 ⊢ Ⅎ _ x F
4 ffnfv ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ z ∈ A F ⁡ z ∈ B
5 nfcv ⊢ Ⅎ _ z A
6 nfcv ⊢ Ⅎ _ x z
7 3 6 nffv ⊢ Ⅎ _ x F ⁡ z
8 7 2 nfel ⊢ Ⅎ x F ⁡ z ∈ B
9 nfv ⊢ Ⅎ z F ⁡ x ∈ B
10 fveq2 ⊢ z = x → F ⁡ z = F ⁡ x
11 10 eleq1d ⊢ z = x → F ⁡ z ∈ B ↔ F ⁡ x ∈ B
12 5 1 8 9 11 cbvralfw ⊢ ∀ z ∈ A F ⁡ z ∈ B ↔ ∀ x ∈ A F ⁡ x ∈ B
13 12 anbi2i ⊢ F Fn A ∧ ∀ z ∈ A F ⁡ z ∈ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
14 4 13 bitri ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B