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 | |
|
nfrexdg.2 | |
||
nfrexdg.3 | |
||
Assertion | nfrexdg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfrexdg.1 | |
|
2 | nfrexdg.2 | |
|
3 | nfrexdg.3 | |
|
4 | dfrex2 | |
|
5 | 3 | nfnd | |
6 | 1 2 5 | nfrald | |
7 | 6 | nfnd | |
8 | 4 7 | nfxfrd | |