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