This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Avoid ax-9 , ax-ext . (Revised by GG, 24-Sep-2024)

	Ref	Expression
Hypotheses	nfraldw.1	$⊢ Ⅎ y φ$
	nfraldw.2	$⊢ φ \to \underline{Ⅎ} x A$
	nfraldw.3	$⊢ φ \to Ⅎ x ψ$
Assertion	nfraldw	$⊢ φ \to Ⅎ x \forall y \in A ψ$

Proof

Step	Hyp	Ref	Expression
1		nfraldw.1	$⊢ Ⅎ y φ$
2		nfraldw.2	$⊢ φ \to \underline{Ⅎ} x A$
3		nfraldw.3	$⊢ φ \to Ⅎ x ψ$
4		df-ral	$⊢ \forall y \in A ψ \leftrightarrow \forall y (y \in A \to ψ)$
5	2	nfcrd	$⊢ φ \to Ⅎ x y \in A$
6	5 3	nfimd	$⊢ φ \to Ⅎ x (y \in A \to ψ)$
7	1 6	nfald	$⊢ φ \to Ⅎ x \forall y (y \in A \to ψ)$
8	4 7	nfxfrd	$⊢ φ \to Ⅎ x \forall y \in A ψ$