Description: Deduction version of nfrexw . (Contributed by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See nfrexd for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfraldw.1 | |- F/ y ph |
|
nfraldw.2 | |- ( ph -> F/_ x A ) |
||
nfraldw.3 | |- ( ph -> F/ x ps ) |
||
Assertion | nfrexdw | |- ( ph -> F/ x E. 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 | dfrex2 | |- ( E. y e. A ps <-> -. A. y e. A -. ps ) |
|
5 | 3 | nfnd | |- ( ph -> F/ x -. ps ) |
6 | 1 2 5 | nfraldw | |- ( ph -> F/ x A. y e. A -. ps ) |
7 | 6 | nfnd | |- ( ph -> F/ x -. A. y e. A -. ps ) |
8 | 4 7 | nfxfrd | |- ( ph -> F/ x E. y e. A ps ) |