Step |
Hyp |
Ref |
Expression |
1 |
|
fmptdF.p |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
fmptdF.a |
⊢ Ⅎ 𝑥 𝐴 |
3 |
|
fmptdF.c |
⊢ Ⅎ 𝑥 𝐶 |
4 |
|
fmptdF.1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 ) |
5 |
|
fmptdF.2 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
6 |
4
|
sbimi |
⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → [ 𝑦 / 𝑥 ] 𝐵 ∈ 𝐶 ) |
7 |
|
sban |
⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝐴 ) ) |
8 |
1
|
sbf |
⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) |
9 |
2
|
clelsb3fw |
⊢ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) |
10 |
8 9
|
anbi12i |
⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) |
11 |
7 10
|
bitri |
⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) |
12 |
|
sbsbc |
⊢ ( [ 𝑦 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ [ 𝑦 / 𝑥 ] 𝐵 ∈ 𝐶 ) |
13 |
|
sbcel12 |
⊢ ( [ 𝑦 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) |
14 |
|
vex |
⊢ 𝑦 ∈ V |
15 |
14 3
|
csbgfi |
⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = 𝐶 |
16 |
15
|
eleq2i |
⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝐶 ) |
17 |
13 16
|
bitri |
⊢ ( [ 𝑦 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝐶 ) |
18 |
12 17
|
bitri |
⊢ ( [ 𝑦 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝐶 ) |
19 |
6 11 18
|
3imtr3i |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝐶 ) |
20 |
19
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝐶 ) |
21 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐴 |
22 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐵 |
23 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 |
24 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
25 |
2 21 22 23 24
|
cbvmptf |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
26 |
25
|
fmpt |
⊢ ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 ) |
27 |
20 26
|
sylib |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 ) |
28 |
5
|
feq1i |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 ) |
29 |
27 28
|
sylibr |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 ) |