Step |
Hyp |
Ref |
Expression |
1 |
|
funcnvmpt.0 |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
funcnvmpt.1 |
⊢ Ⅎ 𝑥 𝐴 |
3 |
|
funcnvmpt.2 |
⊢ Ⅎ 𝑥 𝐹 |
4 |
|
funcnvmpt.3 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
5 |
|
funcnvmpt.4 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) |
6 |
|
nfv |
⊢ Ⅎ 𝑖 𝜑 |
7 |
|
nfcv |
⊢ Ⅎ 𝑖 𝐴 |
8 |
|
nfcv |
⊢ Ⅎ 𝑖 𝐹 |
9 |
|
nfcv |
⊢ Ⅎ 𝑖 𝐵 |
10 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑖 / 𝑥 ⦌ 𝐵 |
11 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) |
12 |
2 7 9 10 11
|
cbvmptf |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) |
13 |
4 12
|
eqtri |
⊢ 𝐹 = ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) |
14 |
5
|
sbimi |
⊢ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → [ 𝑖 / 𝑥 ] 𝐵 ∈ 𝑉 ) |
15 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑖 |
16 |
15 2
|
nfel |
⊢ Ⅎ 𝑥 𝑖 ∈ 𝐴 |
17 |
1 16
|
nfan |
⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) |
18 |
|
eleq1w |
⊢ ( 𝑥 = 𝑖 → ( 𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴 ) ) |
19 |
18
|
anbi2d |
⊢ ( 𝑥 = 𝑖 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ) ) |
20 |
17 19
|
sbiev |
⊢ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ) |
21 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑉 |
22 |
10 21
|
nfel |
⊢ Ⅎ 𝑥 ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∈ 𝑉 |
23 |
11
|
eleq1d |
⊢ ( 𝑥 = 𝑖 → ( 𝐵 ∈ 𝑉 ↔ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) ) |
24 |
22 23
|
sbiev |
⊢ ( [ 𝑖 / 𝑥 ] 𝐵 ∈ 𝑉 ↔ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) |
25 |
14 20 24
|
3imtr3i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) |
26 |
|
csbeq1 |
⊢ ( 𝑖 = 𝑗 → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 = ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) |
27 |
6 7 8 13 25 26
|
funcnv5mpt |
⊢ ( 𝜑 → ( Fun ◡ 𝐹 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) ) ) |