Description: Deduction version of nfralw . Version of nfrald with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 15-Feb-2013) (Revised by Gino Giotto, 10-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfraldw.1 | |- F/ y ph |
|
nfraldw.2 | |- ( ph -> F/_ x A ) |
||
nfraldw.3 | |- ( ph -> F/ x ps ) |
||
Assertion | nfraldw | |- ( ph -> F/ x A. y e. A ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfraldw.1 | |- F/ y ph |
|
2 | nfraldw.2 | |- ( ph -> F/_ x A ) |
|
3 | nfraldw.3 | |- ( ph -> F/ x ps ) |
|
4 | df-ral | |- ( A. y e. A ps <-> A. y ( y e. A -> ps ) ) |
|
5 | nfcvd | |- ( ph -> F/_ x y ) |
|
6 | 5 2 | nfeld | |- ( ph -> F/ x y e. A ) |
7 | 6 3 | nfimd | |- ( ph -> F/ x ( y e. A -> ps ) ) |
8 | 1 7 | nfald | |- ( ph -> F/ x A. y ( y e. A -> ps ) ) |
9 | 4 8 | nfxfrd | |- ( ph -> F/ x A. y e. A ps ) |