Metamath Proof Explorer


Theorem nfrexdg

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 yφ
nfrexdg.2 φ_xA
nfrexdg.3 φxψ
Assertion nfrexdg φxyAψ

Proof

Step Hyp Ref Expression
1 nfrexdg.1 yφ
2 nfrexdg.2 φ_xA
3 nfrexdg.3 φxψ
4 dfrex2 yAψ¬yA¬ψ
5 3 nfnd φx¬ψ
6 1 2 5 nfrald φxyA¬ψ
7 6 nfnd φx¬yA¬ψ
8 4 7 nfxfrd φxyAψ