nfriotad

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

	Ref	Expression
Hypotheses	nfriotad.1	$⊢ Ⅎ y φ$
	nfriotad.2	$⊢ φ \to Ⅎ x ψ$
	nfriotad.3	$⊢ φ \to \underline{Ⅎ} x A$
Assertion	nfriotad	$⊢ φ \to \underline{Ⅎ} x (ι y \in A \| ψ)$

Proof

Step	Hyp	Ref	Expression
1		nfriotad.1	$⊢ Ⅎ y φ$
2		nfriotad.2	$⊢ φ \to Ⅎ x ψ$
3		nfriotad.3	$⊢ φ \to \underline{Ⅎ} x A$
4		df-riota	$⊢ (ι y \in A \| ψ) = (ι y \| (y \in A \land ψ))$
5		nfnae	$⊢ Ⅎ y \neg \forall x x = y$
6	1 5	nfan	$⊢ Ⅎ y (φ \land \neg \forall x x = y)$
7		nfcvf	$⊢ \neg \forall x x = y \to \underline{Ⅎ} x y$
8	7	adantl	$⊢ (φ \land \neg \forall x x = y) \to \underline{Ⅎ} x y$
9	3	adantr	$⊢ (φ \land \neg \forall x x = y) \to \underline{Ⅎ} x A$
10	8 9	nfeld	$⊢ (φ \land \neg \forall x x = y) \to Ⅎ x y \in A$
11	2	adantr	$⊢ (φ \land \neg \forall x x = y) \to Ⅎ x ψ$
12	10 11	nfand	$⊢ (φ \land \neg \forall x x = y) \to Ⅎ x (y \in A \land ψ)$
13	6 12	nfiotad	$⊢ (φ \land \neg \forall x x = y) \to \underline{Ⅎ} x (ι y \| (y \in A \land ψ))$
14	13	ex	$⊢ φ \to (\neg \forall x x = y \to \underline{Ⅎ} x (ι y \| (y \in A \land ψ)))$
15		nfiota1	$⊢ \underline{Ⅎ} y (ι y \| (y \in A \land ψ))$
16		eqidd	$⊢ \forall x x = y \to (ι y \| (y \in A \land ψ)) = (ι y \| (y \in A \land ψ))$
17	16	drnfc1	$⊢ \forall x x = y \to (\underline{Ⅎ} x (ι y \| (y \in A \land ψ)) \leftrightarrow \underline{Ⅎ} y (ι y \| (y \in A \land ψ)))$
18	15 17	mpbiri	$⊢ \forall x x = y \to \underline{Ⅎ} x (ι y \| (y \in A \land ψ))$
19	14 18	pm2.61d2	$⊢ φ \to \underline{Ⅎ} x (ι y \| (y \in A \land ψ))$
20	4 19	nfcxfrd	$⊢ φ \to \underline{Ⅎ} x (ι y \in A \| ψ)$

Metamath Proof Explorer

Theorem nfriotad

Proof