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

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 ⊢ Ⅎ 𝑥 𝐴
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 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )