nfrald

Description: Deduction version of nfral . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfraldw when possible. (Contributed by NM, 15-Feb-2013) (Revised by Mario Carneiro, 7-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfrald.1	$⊢ Ⅎ y φ$
2		nfrald.2	$⊢ φ \to \underline{Ⅎ} x A$
3		nfrald.3	$⊢ φ \to Ⅎ x ψ$
4		df-ral	$⊢ \forall y \in A ψ \leftrightarrow \forall y (y \in A \to ψ)$
5		nfcvf	$⊢ \neg \forall x x = y \to \underline{Ⅎ} x y$
6	5	adantl	$⊢ (φ \land \neg \forall x x = y) \to \underline{Ⅎ} x y$
7	2	adantr	$⊢ (φ \land \neg \forall x x = y) \to \underline{Ⅎ} x A$
8	6 7	nfeld	$⊢ (φ \land \neg \forall x x = y) \to Ⅎ x y \in A$
9	3	adantr	$⊢ (φ \land \neg \forall x x = y) \to Ⅎ x ψ$
10	8 9	nfimd	$⊢ (φ \land \neg \forall x x = y) \to Ⅎ x (y \in A \to ψ)$
11	1 10	nfald2	$⊢ φ \to Ⅎ x \forall y (y \in A \to ψ)$
12	4 11	nfxfrd	$⊢ φ \to Ⅎ x \forall y \in A ψ$

Metamath Proof Explorer

Theorem nfrald

Proof