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	⊢ Ⅎ 𝑦 𝜑
	nfriotad.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
	nfriotad.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion	nfriotad	⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfriotad.1	⊢ Ⅎ 𝑦 𝜑
2		nfriotad.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3		nfriotad.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
4		df-riota	⊢ ( ℩ 𝑦 ∈ 𝐴 𝜓 ) = ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
5		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
6	1 5	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 )
7		nfcvf	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
8	7	adantl	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑦 )
9	3	adantr	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝐴 )
10	8 9	nfeld	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
11	2	adantr	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 )
12	10 11	nfand	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
13	6 12	nfiotad	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
14	13	ex	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
15		nfiota1	⊢ Ⅎ 𝑦 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
16		eqidd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) = ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
17	16	drnfc1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ Ⅎ 𝑦 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
18	15 17	mpbiri	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
19	14 18	pm2.61d2	⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
20	4 19	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 ∈ 𝐴 𝜓 ) )

Metamath Proof Explorer

Theorem nfriotad

Proof