nfriotadw

Description: Deduction version of nfriota with a disjoint variable condition, which contrary to nfriotad does not require ax-13 . (Contributed by NM, 18-Feb-2013) Avoid ax-13 . (Revised by Gino Giotto, 26-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		nfriotadw.1	$⊢ Ⅎ y φ$
2		nfriotadw.2	$⊢ φ \to Ⅎ x ψ$
3		nfriotadw.3	$⊢ φ \to \underline{Ⅎ} x A$
4		df-riota	$⊢ (ι y \in A \| ψ) = (ι y \| (y \in A \land ψ))$
5		nfnaew	$⊢ Ⅎ y \neg \forall x x = y$
6	1 5	nfan	$⊢ Ⅎ y (φ \land \neg \forall x x = y)$
7		nfcvd	$⊢ \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	nfiotadw	$⊢ (φ \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		biidd	$⊢ \forall x x = y \to (w \in (ι y \| (y \in A \land ψ)) \leftrightarrow w \in (ι y \| (y \in A \land ψ)))$
17	16	drnf1v	$⊢ \forall x x = y \to (Ⅎ x w \in (ι y \| (y \in A \land ψ)) \leftrightarrow Ⅎ y w \in (ι y \| (y \in A \land ψ)))$
18	17	albidv	$⊢ \forall x x = y \to (\forall w Ⅎ x w \in (ι y \| (y \in A \land ψ)) \leftrightarrow \forall w Ⅎ y w \in (ι y \| (y \in A \land ψ)))$
19		df-nfc	$⊢ \underline{Ⅎ} x (ι y \| (y \in A \land ψ)) \leftrightarrow \forall w Ⅎ x w \in (ι y \| (y \in A \land ψ))$
20		df-nfc	$⊢ \underline{Ⅎ} y (ι y \| (y \in A \land ψ)) \leftrightarrow \forall w Ⅎ y w \in (ι y \| (y \in A \land ψ))$
21	18 19 20	3bitr4g	$⊢ \forall x x = y \to (\underline{Ⅎ} x (ι y \| (y \in A \land ψ)) \leftrightarrow \underline{Ⅎ} y (ι y \| (y \in A \land ψ)))$
22	15 21	mpbiri	$⊢ \forall x x = y \to \underline{Ⅎ} x (ι y \| (y \in A \land ψ))$
23	14 22	pm2.61d2	$⊢ φ \to \underline{Ⅎ} x (ι y \| (y \in A \land ψ))$
24	4 23	nfcxfrd	$⊢ φ \to \underline{Ⅎ} x (ι y \in A \| ψ)$

Metamath Proof Explorer

Theorem nfriotadw

Proof