Metamath Proof Explorer

Theorem nfrexd

Description: Deduction version of nfrex . (Contributed by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See nfrexdg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

Ref Expression
Hypotheses nfrexd.1 y φ
nfrexd.2 φ _ x A
nfrexd.3 φ x ψ
Assertion nfrexd φ x y A ψ


Step Hyp Ref Expression
1 nfrexd.1 y φ
2 nfrexd.2 φ _ x A
3 nfrexd.3 φ x ψ
4 dfrex2 y A ψ ¬ y A ¬ ψ
5 3 nfnd φ x ¬ ψ
6 1 2 5 nfraldw φ x y A ¬ ψ
7 6 nfnd φ x ¬ y A ¬ ψ
8 4 7 nfxfrd φ x y A ψ