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 | ||
nfiotadw.2 | |||
Assertion | nfiotadw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfiotadw.1 | ||
2 | nfiotadw.2 | ||
3 | dfiota2 | ||
4 | nfv | ||
5 | nfvd | ||
6 | 2 5 | nfbid | |
7 | 1 6 | nfald | |
8 | 4 7 | nfabdw | |
9 | 8 | nfunid | |
10 | 3 9 | nfcxfrd |