Metamath Proof Explorer


Theorem nfrexdw

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 )

Proof

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 )