Description: Deduction version of nfiotaw . Version of nfiotad with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 18-Feb-2013) (Revised by Gino Giotto, 26-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfiotadw.1 | |- F/ y ph |
|
nfiotadw.2 | |- ( ph -> F/ x ps ) |
||
Assertion | nfiotadw | |- ( ph -> F/_ x ( iota y ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfiotadw.1 | |- F/ y ph |
|
2 | nfiotadw.2 | |- ( ph -> F/ x ps ) |
|
3 | dfiota2 | |- ( iota y ps ) = U. { z | A. y ( ps <-> y = z ) } |
|
4 | nfv | |- F/ z ph |
|
5 | nfvd | |- ( ph -> F/ x y = z ) |
|
6 | 2 5 | nfbid | |- ( ph -> F/ x ( ps <-> y = z ) ) |
7 | 1 6 | nfald | |- ( ph -> F/ x A. y ( ps <-> y = z ) ) |
8 | 4 7 | nfabdw | |- ( ph -> F/_ x { z | A. y ( ps <-> y = z ) } ) |
9 | 8 | nfunid | |- ( ph -> F/_ x U. { z | A. y ( ps <-> y = z ) } ) |
10 | 3 9 | nfcxfrd | |- ( ph -> F/_ x ( iota y ps ) ) |