Theorem 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 GG, 26-Jan-2024)

	Ref	Expression
Hypotheses	nfriotadw.1	⊢ Ⅎ 𝑦 𝜑
	nfriotadw.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
	nfriotadw.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion	nfriotadw	⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfriotadw.1	⊢ Ⅎ 𝑦 𝜑
2		nfriotadw.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3		nfriotadw.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
4		df-riota	⊢ ( ℩ 𝑦 ∈ 𝐴 𝜓 ) = ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
5		nfnaew	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
6	1 5	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 )
7		nfcvd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
8	7	adantl	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑦 )
9	3	adantr	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝐴 )
10	8 9	nfeld	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
11	2	adantr	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 )
12	10 11	nfand	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
13	6 12	nfiotadw	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
14	13	ex	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
15		nfiota1	⊢ Ⅎ 𝑦 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
16		biidd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
17	16	drnf1v	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ Ⅎ 𝑦 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
18	17	albidv	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑤 Ⅎ 𝑥 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑤 Ⅎ 𝑦 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
19		df-nfc	⊢ ( Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑤 Ⅎ 𝑥 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
20		df-nfc	⊢ ( Ⅎ 𝑦 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑤 Ⅎ 𝑦 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
21	18 19 20	3bitr4g	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ Ⅎ 𝑦 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
22	15 21	mpbiri	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
23	14 22	pm2.61d2	⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
24	4 23	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 ∈ 𝐴 𝜓 ) )