Theorem nfralw

Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 1-Sep-1999) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024) (Proof shortened by Wolf Lammen, 13-Dec-2024)

	Ref	Expression
Hypotheses	nfralw.1	⊢ Ⅎ 𝑥 𝐴
	nfralw.2	⊢ Ⅎ 𝑥 𝜑
Assertion	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 𝜑

Proof

Step	Hyp	Ref	Expression
1		nfralw.1	⊢ Ⅎ 𝑥 𝐴
2		nfralw.2	⊢ Ⅎ 𝑥 𝜑
3	1	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
4	3	nf5ri	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
5	2	nf5ri	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
6	4 5	hbral	⊢ ( ∀ 𝑦 ∈ 𝐴 𝜑 → ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 𝜑 )
7	6	nf5i	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 𝜑