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	⊢ Ⅎ 𝑥 𝐴
	ffnfvf.2	⊢ Ⅎ 𝑥 𝐵
	ffnfvf.3	⊢ Ⅎ 𝑥 𝐹
Assertion	ffnfvf	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ffnfvf.1	⊢ Ⅎ 𝑥 𝐴
2		ffnfvf.2	⊢ Ⅎ 𝑥 𝐵
3		ffnfvf.3	⊢ Ⅎ 𝑥 𝐹
4		ffnfv	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 ) )
5		nfcv	⊢ Ⅎ 𝑧 𝐴
6		nfcv	⊢ Ⅎ 𝑥 𝑧
7	3 6	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
8	7 2	nfel	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) ∈ 𝐵
9		nfv	⊢ Ⅎ 𝑧 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵
10		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
11	10	eleq1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
12	5 1 8 9 11	cbvralfw	⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
13	12	anbi2i	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
14	4 13	bitri	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )