Description: Deduction version of nfrexg . Usage of this theorem is discouraged because it depends on ax-13 . See nfrexd for a version with a disjoint variable condition, but not requiring ax-13 . (Contributed by Mario Carneiro, 14-Oct-2016) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfrexdg.1 | |- F/ y ph |
|
nfrexdg.2 | |- ( ph -> F/_ x A ) |
||
nfrexdg.3 | |- ( ph -> F/ x ps ) |
||
Assertion | nfrexdg | |- ( ph -> F/ x E. y e. A ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfrexdg.1 | |- F/ y ph |
|
2 | nfrexdg.2 | |- ( ph -> F/_ x A ) |
|
3 | nfrexdg.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 | nfrald | |- ( 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 ) |