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