Step |
Hyp |
Ref |
Expression |
1 |
|
suppval |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } ) |
2 |
1
|
3adant1 |
⊢ ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } ) |
3 |
|
funfn |
⊢ ( Fun 𝑋 ↔ 𝑋 Fn dom 𝑋 ) |
4 |
3
|
biimpi |
⊢ ( Fun 𝑋 → 𝑋 Fn dom 𝑋 ) |
5 |
4
|
3ad2ant1 |
⊢ ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑋 Fn dom 𝑋 ) |
6 |
|
fnsnfv |
⊢ ( ( 𝑋 Fn dom 𝑋 ∧ 𝑖 ∈ dom 𝑋 ) → { ( 𝑋 ‘ 𝑖 ) } = ( 𝑋 “ { 𝑖 } ) ) |
7 |
5 6
|
sylan |
⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → { ( 𝑋 ‘ 𝑖 ) } = ( 𝑋 “ { 𝑖 } ) ) |
8 |
7
|
eqcomd |
⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( 𝑋 “ { 𝑖 } ) = { ( 𝑋 ‘ 𝑖 ) } ) |
9 |
8
|
neeq1d |
⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } ↔ { ( 𝑋 ‘ 𝑖 ) } ≠ { 𝑍 } ) ) |
10 |
|
fvex |
⊢ ( 𝑋 ‘ 𝑖 ) ∈ V |
11 |
|
sneqbg |
⊢ ( ( 𝑋 ‘ 𝑖 ) ∈ V → ( { ( 𝑋 ‘ 𝑖 ) } = { 𝑍 } ↔ ( 𝑋 ‘ 𝑖 ) = 𝑍 ) ) |
12 |
10 11
|
mp1i |
⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( { ( 𝑋 ‘ 𝑖 ) } = { 𝑍 } ↔ ( 𝑋 ‘ 𝑖 ) = 𝑍 ) ) |
13 |
12
|
necon3bid |
⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( { ( 𝑋 ‘ 𝑖 ) } ≠ { 𝑍 } ↔ ( 𝑋 ‘ 𝑖 ) ≠ 𝑍 ) ) |
14 |
9 13
|
bitrd |
⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } ↔ ( 𝑋 ‘ 𝑖 ) ≠ 𝑍 ) ) |
15 |
14
|
rabbidva |
⊢ ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑖 ) ≠ 𝑍 } ) |
16 |
2 15
|
eqtrd |
⊢ ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑖 ) ≠ 𝑍 } ) |