Metamath Proof Explorer

Theorem nfraldw

Description: Deduction version of nfralw . Version of nfrald with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 15-Feb-2013) (Revised by Gino Giotto, 10-Jan-2024)

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


Step Hyp Ref Expression
1 nfraldw.1 y φ
2 nfraldw.2 φ _ x A
3 nfraldw.3 φ x ψ
4 df-ral y A ψ y y A ψ
5 nfcvd φ _ x y
6 5 2 nfeld φ x y A
7 6 3 nfimd φ x y A ψ
8 1 7 nfald φ x y y A ψ
9 4 8 nfxfrd φ x y A ψ