Step |
Hyp |
Ref |
Expression |
1 |
|
fmptf.1 |
⊢ Ⅎ 𝑥 𝐵 |
2 |
|
fmptf.2 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) |
3 |
|
nfv |
⊢ Ⅎ 𝑦 𝐶 ∈ 𝐵 |
4 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 |
5 |
4 1
|
nfel |
⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 |
6 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) |
7 |
6
|
eleq1d |
⊢ ( 𝑥 = 𝑦 → ( 𝐶 ∈ 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) ) |
8 |
3 5 7
|
cbvralw |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) |
9 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐶 |
10 |
9 4 6
|
cbvmpt |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) |
11 |
2 10
|
eqtri |
⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) |
12 |
11
|
fmpt |
⊢ ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) |
13 |
8 12
|
bitri |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) |